%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : LCL017-1 : TPTP v8.1.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Sun Jul 17 14:27:23 EDT 2022
% Result : Unsatisfiable 50.63s 50.80s
% Output : Refutation 50.63s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : LCL017-1 : TPTP v8.1.0. Released v1.0.0.
% 0.07/0.12 % Command : sos-script %s
% 0.13/0.33 % Computer : n006.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Sat Jul 2 16:33:52 EDT 2022
% 0.13/0.33 % CPUTime :
% 0.13/0.35 ----- Otter 3.2, August 2001 -----
% 0.13/0.35 The process was started by sandbox on n006.cluster.edu,
% 0.13/0.35 Sat Jul 2 16:33:52 2022
% 0.13/0.35 The command was "./sos". The process ID is 21385.
% 0.13/0.35
% 0.13/0.35 set(prolog_style_variables).
% 0.13/0.35 set(auto).
% 0.13/0.35 dependent: set(auto1).
% 0.13/0.35 dependent: set(process_input).
% 0.13/0.35 dependent: clear(print_kept).
% 0.13/0.35 dependent: clear(print_new_demod).
% 0.13/0.35 dependent: clear(print_back_demod).
% 0.13/0.35 dependent: clear(print_back_sub).
% 0.13/0.35 dependent: set(control_memory).
% 0.13/0.35 dependent: assign(max_mem, 12000).
% 0.13/0.35 dependent: assign(pick_given_ratio, 4).
% 0.13/0.35 dependent: assign(stats_level, 1).
% 0.13/0.35 dependent: assign(pick_semantic_ratio, 3).
% 0.13/0.35 dependent: assign(sos_limit, 5000).
% 0.13/0.35 dependent: assign(max_weight, 60).
% 0.13/0.35 clear(print_given).
% 0.13/0.35
% 0.13/0.35 list(usable).
% 0.13/0.35
% 0.13/0.35 SCAN INPUT: prop=0, horn=1, equality=0, symmetry=0, max_lits=3.
% 0.13/0.35
% 0.13/0.35 This is a Horn set without equality. The strategy will
% 0.13/0.35 be hyperresolution, with satellites in sos and nuclei
% 0.13/0.35 in usable.
% 0.13/0.35
% 0.13/0.35 dependent: set(hyper_res).
% 0.13/0.35 dependent: clear(order_hyper).
% 0.13/0.35
% 0.13/0.35 ------------> process usable:
% 0.13/0.35
% 0.13/0.35 ------------> process sos:
% 0.13/0.35
% 0.13/0.35 ======= end of input processing =======
% 0.13/0.38
% 0.13/0.38 Model 1 (0.00 seconds, 0 Inserts)
% 0.13/0.38
% 0.13/0.38 Stopped by limit on number of solutions
% 0.13/0.38
% 0.13/0.38
% 0.13/0.38 -------------- Softie stats --------------
% 0.13/0.38
% 0.13/0.38 UPDATE_STOP: 300
% 0.13/0.38 SFINDER_TIME_LIMIT: 2
% 0.13/0.38 SHORT_CLAUSE_CUTOFF: 4
% 0.13/0.38 number of clauses in intial UL: 2
% 0.13/0.38 number of clauses initially in problem: 3
% 0.13/0.38 percentage of clauses intially in UL: 66
% 0.13/0.38 percentage of distinct symbols occuring in initial UL: 100
% 0.13/0.38 percent of all initial clauses that are short: 100
% 0.13/0.38 absolute distinct symbol count: 5
% 0.13/0.38 distinct predicate count: 1
% 0.13/0.38 distinct function count: 1
% 0.13/0.38 distinct constant count: 3
% 0.13/0.38
% 0.13/0.38 ---------- no more Softie stats ----------
% 0.13/0.38
% 0.13/0.38
% 0.13/0.38
% 0.13/0.38 =========== start of search ===========
% 13.13/13.29
% 13.13/13.29
% 13.13/13.29 Changing weight limit from 60 to 56.
% 13.13/13.29
% 13.13/13.29 Model 2 (0.00 seconds, 0 Inserts)
% 13.13/13.29
% 13.13/13.29 Stopped by limit on number of solutions
% 13.13/13.29
% 13.13/13.29 Model 3 (0.00 seconds, 0 Inserts)
% 13.13/13.29
% 13.13/13.29 Stopped by limit on number of solutions
% 13.13/13.29
% 13.13/13.29 Model 4 (0.00 seconds, 0 Inserts)
% 13.13/13.29
% 13.13/13.29 Stopped by limit on number of solutions
% 13.13/13.29
% 13.13/13.29 Resetting weight limit to 56 after 80 givens.
% 13.13/13.29
% 13.73/13.91
% 13.73/13.91
% 13.73/13.91 Changing weight limit from 56 to 48.
% 13.73/13.91
% 13.73/13.91 Resetting weight limit to 48 after 85 givens.
% 13.73/13.91
% 14.57/14.76
% 14.57/14.76
% 14.57/14.76 Changing weight limit from 48 to 44.
% 14.57/14.76
% 14.57/14.76 Resetting weight limit to 44 after 95 givens.
% 14.57/14.76
% 16.83/16.99
% 16.83/16.99
% 16.83/16.99 Changing weight limit from 44 to 40.
% 16.83/16.99
% 16.83/16.99 Model 5 (0.00 seconds, 0 Inserts)
% 16.83/16.99
% 16.83/16.99 Stopped by limit on number of solutions
% 16.83/16.99
% 16.83/16.99 Resetting weight limit to 40 after 100 givens.
% 16.83/16.99
% 17.33/17.54
% 17.33/17.54
% 17.33/17.54 Changing weight limit from 40 to 32.
% 17.33/17.54
% 17.33/17.54 Resetting weight limit to 32 after 110 givens.
% 17.33/17.54
% 20.92/21.12
% 20.92/21.12
% 20.92/21.12 Changing weight limit from 32 to 28.
% 20.92/21.12
% 20.92/21.12 Model 6 [ 7 1 58 ] (0.00 seconds, 189883 Inserts)
% 20.92/21.12
% 20.92/21.12 Resetting weight limit to 28 after 115 givens.
% 20.92/21.12
% 24.69/24.87
% 24.69/24.87
% 24.69/24.87 Changing weight limit from 28 to 29.
% 24.69/24.87
% 24.69/24.87 Model 7 [ 1 0 1086 ] (0.00 seconds, 183746 Inserts)
% 24.69/24.87
% 24.69/24.87 Resetting weight limit to 29 after 125 givens.
% 24.69/24.87
% 24.69/24.90
% 24.69/24.90
% 24.69/24.90 Changing weight limit from 29 to 30.
% 24.69/24.90
% 24.69/24.90 Resetting weight limit to 30 after 130 givens.
% 24.69/24.90
% 24.80/25.00
% 24.80/25.00
% 24.80/25.00 Changing weight limit from 30 to 28.
% 24.80/25.00
% 24.80/25.00 Resetting weight limit to 28 after 145 givens.
% 24.80/25.00
% 32.26/32.45
% 32.26/32.45
% 32.26/32.45 Changing weight limit from 28 to 24.
% 32.26/32.45
% 32.26/32.45 Model 8 [ 4 1 255 ] (0.00 seconds, 175475 Inserts)
% 32.26/32.45
% 32.26/32.45 Resetting weight limit to 24 after 180 givens.
% 32.26/32.45
% 49.37/49.55
% 49.37/49.55
% 49.37/49.55 Changing weight limit from 24 to 20.
% 49.37/49.55
% 49.37/49.55 Model 9 [ 4 0 686 ] (0.00 seconds, 183689 Inserts)
% 49.37/49.55
% 49.37/49.55 Model 10 [ 14 1 717 ] (0.00 seconds, 185755 Inserts)
% 49.37/49.55
% 49.37/49.55 Modelling stopped after 300 given clauses and 0.00 seconds
% 49.37/49.55
% 49.37/49.55
% 49.37/49.55 Resetting weight limit to 20 after 500 givens.
% 49.37/49.55
% 50.63/50.80
% 50.63/50.80 -- HEY sandbox, WE HAVE A PROOF!! --
% 50.63/50.80
% 50.63/50.80 ----> UNIT CONFLICT at 50.34 sec ----> 91452 [binary,91451.1,2.1] {-} $F.
% 50.63/50.80
% 50.63/50.80 Length of proof is 53. Level of proof is 27.
% 50.63/50.80
% 50.63/50.80 ---------------- PROOF ----------------
% 50.63/50.80 % SZS status Unsatisfiable
% 50.63/50.80 % SZS output start Refutation
% 50.63/50.80
% 50.63/50.80 1 [] {+} -is_a_theorem(equivalent(A,B))| -is_a_theorem(A)|is_a_theorem(B).
% 50.63/50.80 2 [] {+} -is_a_theorem(equivalent(equivalent(a,b),equivalent(c,equivalent(equivalent(c,b),a)))).
% 50.63/50.80 3 [] {-} is_a_theorem(equivalent(equivalent(equivalent(A,equivalent(B,C)),C),equivalent(B,A))).
% 50.63/50.80 4 [hyper,3,1,3] {-} is_a_theorem(equivalent(A,equivalent(B,equivalent(C,equivalent(A,equivalent(C,B)))))).
% 50.63/50.80 5 [hyper,4,1,4] {-} is_a_theorem(equivalent(A,equivalent(B,equivalent(equivalent(C,equivalent(D,equivalent(E,equivalent(C,equivalent(E,D))))),equivalent(B,A))))).
% 50.63/50.80 6 [hyper,4,1,3] {-} is_a_theorem(equivalent(A,equivalent(B,equivalent(equivalent(equivalent(equivalent(C,equivalent(D,E)),E),equivalent(D,C)),equivalent(B,A))))).
% 50.63/50.80 9 [hyper,5,1,4] {-} is_a_theorem(equivalent(A,equivalent(equivalent(B,equivalent(C,equivalent(D,equivalent(B,equivalent(D,C))))),equivalent(A,equivalent(E,equivalent(F,equivalent(G,equivalent(E,equivalent(G,F))))))))).
% 50.63/50.80 15 [hyper,6,1,4] {-} is_a_theorem(equivalent(A,equivalent(equivalent(equivalent(equivalent(B,equivalent(C,D)),D),equivalent(C,B)),equivalent(A,equivalent(E,equivalent(F,equivalent(G,equivalent(E,equivalent(G,F))))))))).
% 50.63/50.80 16 [hyper,6,1,3] {-} is_a_theorem(equivalent(A,equivalent(equivalent(equivalent(equivalent(B,equivalent(C,D)),D),equivalent(C,B)),equivalent(A,equivalent(equivalent(equivalent(E,equivalent(F,G)),G),equivalent(F,E)))))).
% 50.63/50.80 44 [hyper,9,1,4] {-} is_a_theorem(equivalent(equivalent(A,equivalent(B,equivalent(C,equivalent(A,equivalent(C,B))))),equivalent(equivalent(D,equivalent(E,equivalent(F,equivalent(D,equivalent(F,E))))),equivalent(G,equivalent(H,equivalent(I,equivalent(G,equivalent(I,H)))))))).
% 50.63/50.80 259 [hyper,44,1,3] {-} is_a_theorem(equivalent(equivalent(A,equivalent(B,equivalent(A,equivalent(C,equivalent(D,equivalent(E,equivalent(C,equivalent(E,D)))))))),B)).
% 50.63/50.80 286 [hyper,259,1,3] {-} is_a_theorem(equivalent(equivalent(A,equivalent(B,equivalent(C,equivalent(D,equivalent(B,equivalent(D,C)))))),A)).
% 50.63/50.80 287 [hyper,259,1,4] {+} is_a_theorem(equivalent(A,equivalent(B,equivalent(A,B)))).
% 50.63/50.80 288 [hyper,287,1,287] {+} is_a_theorem(equivalent(A,equivalent(equivalent(B,equivalent(C,equivalent(B,C))),A))).
% 50.63/50.80 354 [hyper,286,1,15] {-} is_a_theorem(equivalent(A,equivalent(A,equivalent(equivalent(equivalent(B,equivalent(C,D)),D),equivalent(C,B))))).
% 50.63/50.80 360 [hyper,286,1,3] {-} is_a_theorem(equivalent(equivalent(equivalent(A,equivalent(B,equivalent(C,equivalent(B,A)))),equivalent(C,D)),D)).
% 50.63/50.80 534 [hyper,360,1,287] {-} is_a_theorem(equivalent(equivalent(A,equivalent(B,equivalent(C,equivalent(B,A)))),C)).
% 50.63/50.80 535 [hyper,360,1,286] {+} is_a_theorem(equivalent(A,A)).
% 50.63/50.80 571 [hyper,534,1,354] {+} is_a_theorem(equivalent(equivalent(A,equivalent(A,B)),B)).
% 50.63/50.80 626 [hyper,535,1,288] {+} is_a_theorem(equivalent(equivalent(A,equivalent(B,equivalent(A,B))),equivalent(C,C))).
% 50.63/50.80 648 [hyper,535,1,4] {-} is_a_theorem(equivalent(A,equivalent(B,equivalent(equivalent(C,C),equivalent(B,A))))).
% 50.63/50.80 656 [hyper,648,1,286] {+} is_a_theorem(equivalent(A,equivalent(A,equivalent(B,B)))).
% 50.63/50.80 739 [hyper,656,1,571] {+} is_a_theorem(equivalent(equivalent(equivalent(A,equivalent(A,B)),B),equivalent(C,C))).
% 50.63/50.80 2765 [hyper,739,1,3] {-} is_a_theorem(equivalent(A,equivalent(B,equivalent(B,equivalent(A,equivalent(C,C)))))).
% 50.63/50.80 2774 [hyper,2765,1,656] {-} is_a_theorem(equivalent(equivalent(A,equivalent(B,equivalent(B,equivalent(A,equivalent(C,C))))),equivalent(D,D))).
% 50.63/50.80 3648 [hyper,2774,1,3] {+} is_a_theorem(equivalent(equivalent(A,equivalent(B,B)),A)).
% 50.63/50.80 3702 [hyper,3648,1,16] {-} is_a_theorem(equivalent(equivalent(equivalent(A,B),equivalent(equivalent(equivalent(B,equivalent(A,C)),C),D)),D)).
% 50.63/50.80 4541 [hyper,3702,1,739] {-} is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,equivalent(B,A)),C)),C)).
% 50.63/50.80 4544 [hyper,3702,1,626] {-} is_a_theorem(equivalent(equivalent(equivalent(A,equivalent(B,A)),equivalent(B,C)),C)).
% 50.63/50.80 4545 [hyper,3702,1,287] {-} is_a_theorem(equivalent(equivalent(A,B),equivalent(equivalent(B,equivalent(A,C)),C))).
% 50.63/50.80 4603 [hyper,4541,1,287] {+} is_a_theorem(equivalent(A,equivalent(B,equivalent(B,A)))).
% 50.63/50.80 4613 [hyper,4541,1,4] {+} is_a_theorem(equivalent(A,equivalent(B,equivalent(A,equivalent(C,equivalent(C,B)))))).
% 50.63/50.80 5406 [hyper,4544,1,287] {+} is_a_theorem(equivalent(equivalent(A,equivalent(B,A)),B)).
% 50.63/50.80 6382 [hyper,4545,1,5406] {-} is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,equivalent(A,B)),C)),C)).
% 50.63/50.80 6383 [hyper,4545,1,4603] {-} is_a_theorem(equivalent(equivalent(equivalent(A,equivalent(A,B)),equivalent(B,C)),C)).
% 50.63/50.80 7866 [hyper,6382,1,4] {-} is_a_theorem(equivalent(A,equivalent(B,equivalent(A,equivalent(C,equivalent(B,C)))))).
% 50.63/50.80 9472 [hyper,4613,1,4544] {-} is_a_theorem(equivalent(equivalent(A,equivalent(B,A)),equivalent(C,equivalent(C,B)))).
% 50.63/50.80 9663 [hyper,9472,1,3702] {-} is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,B),equivalent(B,C)),C),A)).
% 50.63/50.80 9837 [hyper,9663,1,3] {-} is_a_theorem(equivalent(A,equivalent(equivalent(B,C),equivalent(C,equivalent(A,B))))).
% 50.63/50.80 9854 [hyper,9837,1,4541] {+} is_a_theorem(equivalent(equivalent(A,B),equivalent(B,A))).
% 50.63/50.80 9892 [hyper,9837,1,571] {-} is_a_theorem(equivalent(A,equivalent(equivalent(B,A),B))).
% 50.63/50.80 10047 [hyper,9854,1,4545] {-} is_a_theorem(equivalent(equivalent(equivalent(A,B),equivalent(equivalent(B,A),C)),C)).
% 50.63/50.80 10106 [hyper,9854,1,9472] {-} is_a_theorem(equivalent(equivalent(A,equivalent(A,B)),equivalent(C,equivalent(B,C)))).
% 50.63/50.80 10192 [hyper,9892,1,4545] {-} is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,B),A),equivalent(B,C)),C)).
% 50.63/50.80 11631 [hyper,6383,1,4613] {-} is_a_theorem(equivalent(equivalent(A,equivalent(A,B)),equivalent(C,equivalent(C,B)))).
% 50.63/50.80 14620 [hyper,10047,1,4] {-} is_a_theorem(equivalent(A,equivalent(equivalent(B,C),equivalent(A,equivalent(C,B))))).
% 50.63/50.80 15326 [hyper,10106,1,3702] {-} is_a_theorem(equivalent(A,equivalent(equivalent(equivalent(B,A),equivalent(B,C)),C))).
% 50.63/50.80 18916 [hyper,10192,1,7866] {-} is_a_theorem(equivalent(equivalent(equivalent(A,B),A),equivalent(C,equivalent(B,C)))).
% 50.63/50.80 23708 [hyper,11631,1,3702] {-} is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,B),equivalent(A,C)),C),B)).
% 50.63/50.80 29048 [hyper,14620,1,9854] {-} is_a_theorem(equivalent(equivalent(equivalent(A,B),equivalent(C,equivalent(B,A))),C)).
% 50.63/50.80 34815 [hyper,18916,1,3702] {-} is_a_theorem(equivalent(A,equivalent(equivalent(B,equivalent(equivalent(B,A),C)),C))).
% 50.63/50.80 45115 [hyper,23708,1,3] {-} is_a_theorem(equivalent(A,equivalent(equivalent(B,C),equivalent(B,equivalent(A,C))))).
% 50.63/50.80 49695 [hyper,29048,1,15326] {-} is_a_theorem(equivalent(equivalent(A,equivalent(B,C)),equivalent(A,equivalent(C,B)))).
% 50.63/50.80 62140 [hyper,45115,1,3702] {-} is_a_theorem(equivalent(equivalent(A,equivalent(B,C)),equivalent(equivalent(B,A),C))).
% 50.63/50.80 68746 [hyper,49695,1,34815] {-} is_a_theorem(equivalent(A,equivalent(B,equivalent(C,equivalent(equivalent(C,A),B))))).
% 50.63/50.80 91451 [hyper,68746,1,62140] {-} is_a_theorem(equivalent(equivalent(A,B),equivalent(C,equivalent(equivalent(C,B),A)))).
% 50.63/50.80 91452 [binary,91451.1,2.1] {-} $F.
% 50.63/50.80
% 50.63/50.80 % SZS output end Refutation
% 50.63/50.80 ------------ end of proof -------------
% 50.63/50.80
% 50.63/50.80
% 50.63/50.80 Search stopped by max_proofs option.
% 50.63/50.80
% 50.63/50.80
% 50.63/50.80 Search stopped by max_proofs option.
% 50.63/50.80
% 50.63/50.80 ============ end of search ============
% 50.63/50.80
% 50.63/50.80 ----------- soft-scott stats ----------
% 50.63/50.80
% 50.63/50.80 true clauses given 44 (8.0%)
% 50.63/50.80 false clauses given 504
% 50.63/50.80
% 50.63/50.80 FALSE TRUE
% 50.63/50.80 12 69 74
% 50.63/50.80 16 2526 690
% 50.63/50.80 20 969 1771
% 50.63/50.80 tot: 3564 2535 (41.6% true)
% 50.63/50.80
% 50.63/50.80
% 50.63/50.80 Model 10 [ 14 1 717 ] (0.00 seconds, 185755 Inserts)
% 50.63/50.80
% 50.63/50.80 That finishes the proof of the theorem.
% 50.63/50.80
% 50.63/50.80 Process 21385 finished Sat Jul 2 16:34:43 2022
%------------------------------------------------------------------------------