View difference between Paste ID: DXCg5rYG and jGLY54bN

-Proof:
+
-length = 4, depth = 2
+%               pttp_load_wid(logicmoo_kb_refution).
-Goal#  Wff#  Wff Instance
+
------  ----  ------------
+
-  [0]  query   query :- [1].
+
-  [1]  asserted_t(fatherOf,phil,gun)      asserted_t(fatherOf,phil,gun) :- [2] , [3].
+
-  [2]  asserted_t(sonOf,gun,phil)         asserted_t(sonOf,gun,phil).
+
-  [3]  not_asserted_t(motherOf,phil,gun)         not_asserted_t(motherOf,phil,gun) :- [4].
+
-  [4]  not_asserted_t(female,gun)            not_asserted_t(female,gun).
+
-Proof end.
+
-%    succceeded(dbase_rules_pttp:pttp_prove(logicmoo_example22, query)).
+
 logicmoo_kb_refution:7  unknowable_t(A,B,C);proven_t(A,B,C);refuted_t(A,B,C).
-%               do_pttp_test(logicmoo_example4).
+
 logicmoo_kb_refution:9  not_both_t(secondOrder_t(disjointWith,A,B),proven_t(A,C,D));refuted_t(B,C,D).
-%            pttp_load_wid(logicmoo_kb_refution).
+
 logicmoo_kb_refution:11  not_both_t(secondOrder_t(genlInverse,A,B),proven_t(A,D,C));proven_t(B,C,D).
 logicmoo_kb_refution:12  not_both_t(secondOrder_t(negationPreds,A,B),proven_t(A,C,D));refuted_t(B,C,D).
 logicmoo_kb_refution:13  not_both_t(secondOrder_t(negationInverse,A,B),proven_t(A,D,C));refuted_t(B,C,D).
 logicmoo_kb_refution:14  not_both_t(secondOrder_isa_t(transitive,A), (proven_t(A,C,B),proven_t(A,B,D)));proven_t(A,C,D).
 logicmoo_kb_refution:15  not_both_t(secondOrder_isa_t(reflexive,A),proven_t(A,C,B));proven_t(A,B,C).
 logicmoo_kb_refution:16  not_both_t(secondOrder_isa_t(symmetric,A),proven_t(A,C,B));proven_t(A,B,C).
 logicmoo_kb_refution:17  not_both_t(secondOrder_isa_t(irreflexive,A),proven_t(A,C,B));refuted_t(A,B,C).
 logicmoo_kb_refution:18  not_both_t(secondOrder_isa_t(irreflexive,A),secondOrder_t(genlInverse,A,B));proven_t(irreflexive,B).
 logicmoo_kb_refution:19  not_both_t(secondOrder_isa_t(irreflexive,A),secondOrder_t(genlPreds,B,A));proven_t(irreflexive,B).
 true.
 
 12 ?- listing_wid(logicmoo_kb_refution).
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %   logicmoo_kb_refution:0
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 % pttp_in: asserted_t(M29, N29, O29)=>proven_t(M29, N29, O29)& -refuted_t(M29, N29, O29)& -unknowable_t(M29, N29, O29).
 
 int_not_asserted_t(_, _, _).
 
 int_proven_t(A, B, C) :-
-logicmoo_example4:1  secondOrder_t(genlInverse,parentOf,sonOf).
+        asserted_t(A, B, C).
-logicmoo_example4:2  secondOrder_t(genlPreds,motherOf,parentOf).
+
-logicmoo_example4:3  secondOrder_isa_t(irreflexive,sonOf).
+int_not_refuted_t(A, B, C) :-
-logicmoo_example4:4  asserted_t(parentOf,son_1,father_1).
+        asserted_t(A, B, C).
-logicmoo_example4:5  query:-refuted_t(sonOf,son_1,father_1).2.5.
+
-% 2,632 inferences, 0.000 CPU in 0.000 seconds (97% CPU, 6136772 Lips)
+int_not_unknowable_t(A, B, C) :-
         asserted_t(A, B, C).
-Proof time: 0.0005372789999995575 seconds
+
-Proof:
+
-length = 6, depth = 3
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-Goal#  Wff#  Wff Instance
+%   logicmoo_kb_refution:1
------  ----  ------------
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  [0]  query   query :- [1].
+
-  [1]  refuted_t(sonOf,son_1,father_1)      refuted_t(sonOf,son_1,father_1) :- [2] , [3].
+% pttp_in: proven_t(M29, N29, O29)=> -refuted_t(M29, N29, O29)& -unknowable_t(M29, N29, O29).
-  [2]  secondOrder_isa_t(irreflexive,sonOf)         secondOrder_isa_t(irreflexive,sonOf).
+
-  [3]  proven_t(sonOf,father_1,son_1)         proven_t(sonOf,father_1,son_1) :- [4] , [5].
+int_not_proven_t(_, _, _).
-  [4]  secondOrder_t(genlInverse,parentOf,sonOf)            secondOrder_t(genlInverse,parentOf,sonOf).
+
-  [5]  proven_t(parentOf,son_1,father_1)            proven_t(parentOf,son_1,father_1) :- [6].
+int_not_refuted_t(A, B, C) :-
-  [6]  asserted_t(parentOf,son_1,father_1)               asserted_t(parentOf,son_1,father_1).
+        proven_t(A, B, C).
-Proof end.
+
-%    succceeded(dbase_rules_pttp:pttp_prove(logicmoo_example4, query)).
+int_not_unknowable_t(A, B, C) :-
         proven_t(A, B, C).
-%               do_pttp_test(logicmoo_example3).
+
 
-%            pttp_load_wid(logicmoo_kb_logic).
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %   logicmoo_kb_refution:2
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-logicmoo_kb_logic:0  not_asserted_t(A,B,C);proven_t(A,B,C).
+
-logicmoo_kb_logic:1  not_proven_t(A,B,C);possible_t(A,B,C),not_unknowable_t(A,B,C),not_refuted_t(A,B,C).
+% pttp_in: refuted_t(M29, N29, O29)=> -proven_t(M29, N29, O29)& -asserted_t(M29, N29, O29)& -unknowable_t(M29, N29, O29).
-logicmoo_kb_logic:2  not_possible_t(A,B,C);not_refuted_t(A,B,C).
+
-logicmoo_kb_logic:3  not_refuted_t(A,B,C);not_proven_t(A,B,C).
+int_not_refuted_t(_, _, _).
-logicmoo_kb_logic:4  not_unknowable_t(A,B,C);not_proven_t(A,B,C),not_asserted_t(A,B,C),not_refuted_t(A,B,C).
+
-logicmoo_kb_logic:5  asserted_t(A,B,C);not_proven_t(A,B,C).
+int_not_proven_t(A, B, C) :-
-logicmoo_kb_logic:6  proven_t(A,B,C);not_asserted_t(A,B,C).
+        refuted_t(A, B, C).
-logicmoo_kb_logic:7  possible_t(A,B,C);refuted_t(A,B,C).
+
-logicmoo_kb_logic:8  refuted_t(A,B,C);possible_t(A,B,C).
+int_not_asserted_t(A, B, C) :-
-logicmoo_kb_logic:9  unknowable_t(A,B,C);possible_t(A,B,C).
+        refuted_t(A, B, C).
-logicmoo_kb_logic:10  not_both_t(secondOrder_t(genls,A,B),secondOrder_isa_t(A,C));secondOrder_isa_t(B,C).
+
-logicmoo_kb_logic:11  not_both_t(secondOrder_t(disjointWith,A,B),asserted_t(A,C,D));refuted_t(B,C,D).
+int_not_unknowable_t(A, B, C) :-
-logicmoo_kb_logic:12  not_both_t(secondOrder_t(genlPreds,A,B),asserted_t(A,C,D));proven_t(B,C,D).
+        refuted_t(A, B, C).
-logicmoo_kb_logic:13  not_both_t(secondOrder_t(genlInverse,A,B),asserted_t(A,D,C));proven_t(B,C,D).
+
-logicmoo_kb_logic:14  not_both_t(secondOrder_t(negationPreds,A,B),asserted_t(A,C,D));refuted_t(B,C,D).
+
-logicmoo_kb_logic:15  not_both_t(secondOrder_t(negationInverse,A,B),asserted_t(A,D,C));refuted_t(B,C,D).
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-logicmoo_kb_logic:16  not_both_t(secondOrder_isa_t(transitive,A), (asserted_t(A,C,B),asserted_t(A,B,D)));proven_t(A,C,D).
+%   logicmoo_kb_refution:3
-logicmoo_kb_logic:17  not_secondOrder_isa_t(reflexive,A);proven_t(A,B,B).
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-logicmoo_kb_logic:18  not_both_t(secondOrder_isa_t(symmetric,A),asserted_t(A,C,B));proven_t(A,B,C).
+
-logicmoo_kb_logic:19  not_both_t(secondOrder_isa_t(irreflexive,A),asserted_t(A,C,B));not_asserted_t(A,B,C).
+% pttp_in: unknowable_t(M29, N29, O29)=> -proven_t(M29, N29, O29)& -asserted_t(M29, N29, O29)& -refuted_t(M29, N29, O29).
-logicmoo_kb_logic:20  not_both_t(secondOrder_isa_t(irreflexive,A),secondOrder_t(genlInverse,A,B));proven_t(irreflexive,B).
+
-logicmoo_kb_logic:21  not_both_t(secondOrder_isa_t(irreflexive,A),secondOrder_t(genlPreds,B,A));proven_t(irreflexive,B).
+int_not_unknowable_t(_, _, _).
-logicmoo_example3:1  secondOrder_t(genlInverse,parentOf,sonOf).
+
-logicmoo_example3:2  secondOrder_t(genlPreds,motherOf,parentOf).
+int_not_proven_t(A, B, C) :-
-logicmoo_example3:3  secondOrder_isa_t(irreflexive,sonOf).
+        unknowable_t(A, B, C).
-logicmoo_example3:4  asserted_t(parentOf,son_1,father_1).
+
-logicmoo_example3:5  query:-not_asserted_t(sonOf,son_1,father_1).2.5.
+int_not_asserted_t(A, B, C) :-
-% 3,709 inferences, 0.001 CPU in 0.001 seconds (98% CPU, 6710596 Lips)
+        unknowable_t(A, B, C).
 
-Proof time: 0.0006547660000002509 seconds
+int_not_refuted_t(A, B, C) :-
-Proof:
+        unknowable_t(A, B, C).
-length = 6, depth = 3
+
-Goal#  Wff#  Wff Instance
+
------  ----  ------------
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  [0]  query   query :- [1].
+%   logicmoo_kb_refution:4
-  [1]  not_asserted_t(sonOf,son_1,father_1)      not_asserted_t(sonOf,son_1,father_1) :- [2] , [3].
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  [2]  secondOrder_isa_t(irreflexive,sonOf)         secondOrder_isa_t(irreflexive,sonOf).
+
-  [3]  asserted_t(sonOf,father_1,son_1)         asserted_t(sonOf,father_1,son_1) :- [4].
+% pttp_in: -proven_t(M29, N29, O29)=> -refuted_t(M29, N29, O29)v refuted_t(M29, N29, O29)v unknowable_t(M29, N29, O29).
-  [4]  proven_t(sonOf,father_1,son_1)            proven_t(sonOf,father_1,son_1) :- [5] , [6].
+
-  [5]  secondOrder_t(genlInverse,parentOf,sonOf)               secondOrder_t(genlInverse,parentOf,sonOf).
+int_proven_t(A, B, C) :-
-  [6]  asserted_t(parentOf,son_1,father_1)               asserted_t(parentOf,son_1,father_1).
+        refuted_t(A, B, C),
-Proof end.
+        not_refuted_t(A, B, C),
-%    succceeded(dbase_rules_pttp:pttp_prove(logicmoo_example3, query)).
+        not_unknowable_t(A, B, C).
 
-:- dynamic pttp_test_took/3.
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-pttp_test_took(chang_lee_example1, success, 0.017774654000000112).
+%   logicmoo_kb_refution:5
-pttp_test_took(chang_lee_example2, success, 0.007574271999999382).
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-pttp_test_took(chang_lee_example3, success, 0.0016142770000016071).
+
-pttp_test_took(chang_lee_example4, success, 0.0005561190000022975).
+% pttp_in: -asserted_t(M29, N29, O29)=>refuted_t(M29, N29, O29)v unknowable_t(M29, N29, O29)v-unknowable(M29, N29, O29).
-pttp_test_took(chang_lee_example5, success, 0.0003571740000012369).
+
-pttp_test_took(chang_lee_example6, success, 0.0005447289999978011).
+int_asserted_t(A, B, C) :-
-pttp_test_took(chang_lee_example7, success, 0.0004462469999992891).
+        not_refuted_t(A, B, C),
-pttp_test_took(chang_lee_example8, success, 0.018975419000000215).
+        not_unknowable_t(A, B, C),
-pttp_test_took(chang_lee_example9, success, 0.001030349000000541).
+        asserted_t(unknowable, A, B, C).
-pttp_test_took(logicmoo_example1, success, 0.000303224999999685).
+
-pttp_test_took(logicmoo_example1_holds, success, 0.00029053800000156116).
+int_refuted_t(A, B, C) :-
-pttp_test_took(logicmoo_example1_holds2, failure, 0.00021594500000077232).
+        not_asserted_t(A, B, C),
-pttp_test_took(logicmoo_example2, success, 0.0004661060000010764).
+        not_unknowable_t(A, B, C),
-pttp_test_took(logicmoo_example22, success, 0.0004307779999983552).
+        asserted_t(unknowable, A, B, C).
-pttp_test_took(logicmoo_example4, success, 0.0007900379999981055).
+
-pttp_test_took(logicmoo_example3, success, 0.0009260170000011669).
+int_unknowable_t(A, B, C) :-
         not_asserted_t(A, B, C),
-%       gripe_pttp_failure(logicmoo_example1_holds2).
+        not_refuted_t(A, B, C),
         asserted_t(unknowable, A, B, C).
 
 int_not_asserted_t(unknowable, A, B, C) :-
-2 ?-
+        not_asserted_t(A, B, C),
         not_refuted_t(A, B, C),
         not_unknowable_t(A, B, C).
 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %   logicmoo_kb_refution:6
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 % pttp_in: -refuted_t(M29, N29, O29)=>unknowable_t(M29, N29, O29)v-unknowable_t(M29, N29, O29).
 
 int_refuted_t(A, B, C) :-
         not_unknowable_t(A, B, C),
         unknowable_t(A, B, C).
 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %   logicmoo_kb_refution:7
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 % pttp_in: -unknowable_t(M29, N29, O29)=>proven_t(M29, N29, O29)v refuted_t(M29, N29, O29).
 
 int_unknowable_t(A, B, C) :-
         not_proven_t(A, B, C),
         not_refuted_t(A, B, C).
 
 int_proven_t(A, B, C) :-
         not_unknowable_t(A, B, C),
         not_refuted_t(A, B, C).
 
 int_refuted_t(A, B, C) :-
         not_unknowable_t(A, B, C),
         not_proven_t(A, B, C).
 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %   logicmoo_kb_refution:8
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 % pttp_in: secondOrder_t(genls, M29, N29)&secondOrder_isa_t(M29, O29)=>secondOrder_isa_t(N29, O29).
 
 int_not_both_t(secondOrder_t(genls, _, A), secondOrder_isa_t(_, B)) :-
         not_secondOrder_isa_t(A, B).
 
 int_secondOrder_isa_t(A, C) :-
         secondOrder_t(genls, B, A),
         secondOrder_isa_t(B, C).
 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %   logicmoo_kb_refution:9
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 % pttp_in: secondOrder_t(disjointWith, M29, N29)&proven_t(M29, O29, P29)=>refuted_t(N29, O29, P29).
 
 int_not_both_t(secondOrder_t(disjointWith, _, A), proven_t(_, B, C)) :-
         not_refuted_t(A, B, C).
 
 int_refuted_t(A, C, D) :-
         secondOrder_t(disjointWith, B, A),
         proven_t(B, C, D).
 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %   logicmoo_kb_refution:10
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 % pttp_in: secondOrder_t(genlPreds, M29, N29)&proven_t(M29, O29, P29)=>proven_t(N29, O29, P29).
 
 int_not_both_t(secondOrder_t(genlPreds, _, A), proven_t(_, B, C)) :-
         not_proven_t(A, B, C).
 
 int_proven_t(A, C, D) :-
         secondOrder_t(genlPreds, B, A),
         proven_t(B, C, D).
 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %   logicmoo_kb_refution:11
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 % pttp_in: secondOrder_t(genlInverse, M29, N29)&proven_t(M29, O29, P29)=>proven_t(N29, P29, O29).
 
 int_not_both_t(secondOrder_t(genlInverse, _, A), proven_t(_, C, B)) :-
         not_proven_t(A, B, C).
 
 int_proven_t(A, D, C) :-
         secondOrder_t(genlInverse, B, A),
         proven_t(B, C, D).
 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %   logicmoo_kb_refution:12
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 % pttp_in: secondOrder_t(negationPreds, M29, N29)&proven_t(M29, O29, P29)=>refuted_t(N29, O29, P29).
 
 int_not_both_t(secondOrder_t(negationPreds, _, A), proven_t(_, B, C)) :-
         not_refuted_t(A, B, C).
 
 int_refuted_t(A, C, D) :-
         secondOrder_t(negationPreds, B, A),
         proven_t(B, C, D).
 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %   logicmoo_kb_refution:13
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 % pttp_in: secondOrder_t(negationInverse, M29, N29)&proven_t(M29, O29, P29)=>refuted_t(N29, P29, O29).
 
 int_not_both_t(secondOrder_t(negationInverse, _, A), proven_t(_, C, B)) :-
         not_refuted_t(A, B, C).
 
 int_refuted_t(A, D, C) :-
         secondOrder_t(negationInverse, B, A),
         proven_t(B, C, D).
 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %   logicmoo_kb_refution:14
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 % pttp_in: secondOrder_isa_t(transitive, M29)&proven_t(M29, N29, O29)&proven_t(M29, O29, P29)=>proven_t(M29, N29, P29).
 
 int_not_both_t(secondOrder_isa_t(transitive, A), (proven_t(_, B, _), proven_t(_, _, C))) :-
         not_proven_t(A, B, C).
 
 int_proven_t(A, B, D) :-
         secondOrder_isa_t(transitive, A),
         proven_t(A, B, C),
         proven_t(A, C, D).
 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %   logicmoo_kb_refution:15
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 % pttp_in: secondOrder_isa_t(reflexive, M29)&proven_t(M29, N29, O29)=>proven_t(M29, O29, N29).
 
 int_not_both_t(secondOrder_isa_t(reflexive, A), proven_t(_, C, B)) :-
         not_proven_t(A, B, C).
 
 int_proven_t(A, C, B) :-
         secondOrder_isa_t(reflexive, A),
         proven_t(A, B, C).
 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %   logicmoo_kb_refution:16
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 % pttp_in: secondOrder_isa_t(symmetric, M29)&proven_t(M29, N29, O29)=>proven_t(M29, O29, N29).
 
 int_not_both_t(secondOrder_isa_t(symmetric, A), proven_t(_, C, B)) :-
         not_proven_t(A, B, C).
 
 int_proven_t(A, C, B) :-
         secondOrder_isa_t(symmetric, A),
         proven_t(A, B, C).
 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %   logicmoo_kb_refution:17
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 % pttp_in: secondOrder_isa_t(irreflexive, M29)&proven_t(M29, N29, O29)=>refuted_t(M29, O29, N29).
 
 int_not_both_t(secondOrder_isa_t(irreflexive, A), proven_t(_, C, B)) :-
         not_refuted_t(A, B, C).
 
 int_refuted_t(A, C, B) :-
         secondOrder_isa_t(irreflexive, A),
         proven_t(A, B, C).
 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %   logicmoo_kb_refution:18
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 % pttp_in: secondOrder_isa_t(irreflexive, M29)&secondOrder_t(genlInverse, M29, N29)=>proven_t(irreflexive, N29).
 
 int_not_both_t(secondOrder_isa_t(irreflexive, _), secondOrder_t(genlInverse, _, A)) :-
         not_proven_t(irreflexive, A).
 
 int_proven_t(irreflexive, B) :-
         secondOrder_isa_t(irreflexive, A),
         secondOrder_t(genlInverse, A, B).
 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %   logicmoo_kb_refution:19
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 % pttp_in: secondOrder_isa_t(irreflexive, M29)&secondOrder_t(genlPreds, N29, M29)=>proven_t(irreflexive, N29).
 
 int_not_both_t(secondOrder_isa_t(irreflexive, _), secondOrder_t(genlPreds, A, _)) :-
         not_proven_t(irreflexive, A).
 
 int_proven_t(irreflexive, A) :-
         secondOrder_isa_t(irreflexive, B),
         secondOrder_t(genlPreds, A, B).
 
 true.