%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : LCL020-1 : TPTP v8.1.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n021.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:24 EDT 2022
% Result : Unsatisfiable 266.02s 266.30s
% Output : Refutation 266.02s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : LCL020-1 : TPTP v8.1.0. Released v1.0.0.
% 0.12/0.13 % Command : sos-script %s
% 0.12/0.34 % Computer : n021.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Sun Jul 3 18:06:31 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.19/0.36 ----- Otter 3.2, August 2001 -----
% 0.19/0.36 The process was started by sandbox on n021.cluster.edu,
% 0.19/0.36 Sun Jul 3 18:06:31 2022
% 0.19/0.36 The command was "./sos". The process ID is 17257.
% 0.19/0.36
% 0.19/0.36 set(prolog_style_variables).
% 0.19/0.36 set(auto).
% 0.19/0.36 dependent: set(auto1).
% 0.19/0.36 dependent: set(process_input).
% 0.19/0.36 dependent: clear(print_kept).
% 0.19/0.36 dependent: clear(print_new_demod).
% 0.19/0.36 dependent: clear(print_back_demod).
% 0.19/0.36 dependent: clear(print_back_sub).
% 0.19/0.36 dependent: set(control_memory).
% 0.19/0.36 dependent: assign(max_mem, 12000).
% 0.19/0.36 dependent: assign(pick_given_ratio, 4).
% 0.19/0.36 dependent: assign(stats_level, 1).
% 0.19/0.36 dependent: assign(pick_semantic_ratio, 3).
% 0.19/0.36 dependent: assign(sos_limit, 5000).
% 0.19/0.36 dependent: assign(max_weight, 60).
% 0.19/0.36 clear(print_given).
% 0.19/0.36
% 0.19/0.36 list(usable).
% 0.19/0.36
% 0.19/0.36 SCAN INPUT: prop=0, horn=1, equality=0, symmetry=0, max_lits=3.
% 0.19/0.36
% 0.19/0.36 This is a Horn set without equality. The strategy will
% 0.19/0.36 be hyperresolution, with satellites in sos and nuclei
% 0.19/0.36 in usable.
% 0.19/0.36
% 0.19/0.36 dependent: set(hyper_res).
% 0.19/0.36 dependent: clear(order_hyper).
% 0.19/0.36
% 0.19/0.36 ------------> process usable:
% 0.19/0.36
% 0.19/0.36 ------------> process sos:
% 0.19/0.36
% 0.19/0.36 ======= end of input processing =======
% 0.19/0.38
% 0.19/0.38 Model 1 (0.00 seconds, 0 Inserts)
% 0.19/0.38
% 0.19/0.38 Stopped by limit on number of solutions
% 0.19/0.38
% 0.19/0.38
% 0.19/0.38 -------------- Softie stats --------------
% 0.19/0.38
% 0.19/0.38 UPDATE_STOP: 300
% 0.19/0.38 SFINDER_TIME_LIMIT: 2
% 0.19/0.38 SHORT_CLAUSE_CUTOFF: 4
% 0.19/0.38 number of clauses in intial UL: 2
% 0.19/0.38 number of clauses initially in problem: 3
% 0.19/0.38 percentage of clauses intially in UL: 66
% 0.19/0.38 percentage of distinct symbols occuring in initial UL: 100
% 0.19/0.38 percent of all initial clauses that are short: 100
% 0.19/0.38 absolute distinct symbol count: 5
% 0.19/0.38 distinct predicate count: 1
% 0.19/0.38 distinct function count: 1
% 0.19/0.38 distinct constant count: 3
% 0.19/0.38
% 0.19/0.38 ---------- no more Softie stats ----------
% 0.19/0.38
% 0.19/0.38
% 0.19/0.38
% 0.19/0.38 =========== start of search ===========
% 7.48/7.69
% 7.48/7.69
% 7.48/7.69 Changing weight limit from 60 to 52.
% 7.48/7.69
% 7.48/7.69 Model 2 (0.00 seconds, 0 Inserts)
% 7.48/7.69
% 7.48/7.69 Stopped by limit on number of solutions
% 7.48/7.69
% 7.48/7.69 Resetting weight limit to 52 after 125 givens.
% 7.48/7.69
% 7.73/7.91
% 7.73/7.91
% 7.73/7.91 Changing weight limit from 52 to 48.
% 7.73/7.91
% 7.73/7.91 Resetting weight limit to 48 after 130 givens.
% 7.73/7.91
% 8.83/9.02
% 8.83/9.02
% 8.83/9.02 Changing weight limit from 48 to 44.
% 8.83/9.02
% 8.83/9.02 Resetting weight limit to 44 after 145 givens.
% 8.83/9.02
% 9.72/9.91
% 9.72/9.91
% 9.72/9.91 Changing weight limit from 44 to 40.
% 9.72/9.91
% 9.72/9.91 Resetting weight limit to 40 after 165 givens.
% 9.72/9.91
% 10.88/11.06
% 10.88/11.06
% 10.88/11.06 Changing weight limit from 40 to 32.
% 10.88/11.06
% 10.88/11.06 Resetting weight limit to 32 after 200 givens.
% 10.88/11.06
% 15.08/15.28
% 15.08/15.28
% 15.08/15.28 Changing weight limit from 32 to 28.
% 15.08/15.28
% 15.08/15.28 Modelling stopped after 300 given clauses and 0.00 seconds
% 15.08/15.28
% 15.08/15.28
% 15.08/15.28 Resetting weight limit to 28 after 490 givens.
% 15.08/15.28
% 71.18/71.42
% 71.18/71.42
% 71.18/71.42 Changing weight limit from 28 to 24.
% 71.18/71.42
% 71.18/71.42 Resetting weight limit to 24 after 3620 givens.
% 71.18/71.42
% 266.02/266.30
% 266.02/266.30 -- HEY sandbox, WE HAVE A PROOF!! --
% 266.02/266.30
% 266.02/266.30 ----> UNIT CONFLICT at 260.99 sec ----> 760909 [binary,760908.1,2.1] {-} $F.
% 266.02/266.30
% 266.02/266.30 Length of proof is 102. Level of proof is 48.
% 266.02/266.30
% 266.02/266.30 ---------------- PROOF ----------------
% 266.02/266.30 % SZS status Unsatisfiable
% 266.02/266.30 % SZS output start Refutation
% 266.02/266.30
% 266.02/266.30 1 [] {+} -is_a_theorem(equivalent(A,B))| -is_a_theorem(A)|is_a_theorem(B).
% 266.02/266.30 2 [] {+} -is_a_theorem(equivalent(a,equivalent(equivalent(b,equivalent(c,a)),equivalent(c,b)))).
% 266.02/266.30 3 [] {-} is_a_theorem(equivalent(A,equivalent(equivalent(B,C),equivalent(equivalent(A,C),B)))).
% 266.02/266.30 4 [hyper,3,1,3] {-} is_a_theorem(equivalent(equivalent(A,B),equivalent(equivalent(equivalent(C,equivalent(equivalent(D,E),equivalent(equivalent(C,E),D))),B),A))).
% 266.02/266.30 5 [hyper,4,1,4] {-} is_a_theorem(equivalent(equivalent(equivalent(A,equivalent(equivalent(B,C),equivalent(equivalent(A,C),B))),equivalent(equivalent(equivalent(D,equivalent(equivalent(E,F),equivalent(equivalent(D,F),E))),G),H)),equivalent(H,G))).
% 266.02/266.30 7 [hyper,4,1,3] {-} is_a_theorem(equivalent(equivalent(equivalent(A,equivalent(equivalent(B,C),equivalent(equivalent(A,C),B))),equivalent(equivalent(D,E),equivalent(equivalent(F,E),D))),F)).
% 266.02/266.30 20 [hyper,5,1,7] {-} is_a_theorem(equivalent(equivalent(equivalent(A,B),equivalent(equivalent(equivalent(equivalent(C,equivalent(equivalent(D,E),equivalent(equivalent(C,E),D))),F),B),A)),F)).
% 266.02/266.30 33 [hyper,20,1,4] {-} is_a_theorem(equivalent(equivalent(equivalent(A,equivalent(equivalent(B,C),equivalent(equivalent(A,C),B))),D),equivalent(equivalent(E,F),equivalent(equivalent(equivalent(equivalent(G,equivalent(equivalent(H,I),equivalent(equivalent(G,I),H))),D),F),E)))).
% 266.02/266.30 34 [hyper,20,1,3] {-} is_a_theorem(equivalent(equivalent(A,B),equivalent(equivalent(equivalent(equivalent(equivalent(C,D),equivalent(equivalent(equivalent(equivalent(E,equivalent(equivalent(F,G),equivalent(equivalent(E,G),F))),H),D),C)),H),B),A))).
% 266.02/266.30 87 [hyper,34,1,3] {-} is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(A,B),equivalent(equivalent(equivalent(equivalent(C,equivalent(equivalent(D,E),equivalent(equivalent(C,E),D))),F),B),A)),F),equivalent(equivalent(G,H),equivalent(equivalent(I,H),G))),I)).
% 266.02/266.30 125 [hyper,33,1,20] {-} is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(B,C),equivalent(equivalent(A,C),B))),D),D),equivalent(equivalent(E,F),equivalent(equivalent(G,F),E))),G)).
% 266.02/266.30 150 [hyper,125,1,5] {+} is_a_theorem(equivalent(A,A)).
% 266.02/266.30 153 [hyper,125,1,3] {-} is_a_theorem(equivalent(equivalent(equivalent(A,equivalent(equivalent(B,C),equivalent(equivalent(A,C),B))),D),D)).
% 266.02/266.30 158 [hyper,150,1,3] {-} is_a_theorem(equivalent(equivalent(A,B),equivalent(equivalent(equivalent(C,C),B),A))).
% 266.02/266.30 165 [hyper,158,1,158] {-} is_a_theorem(equivalent(equivalent(equivalent(A,A),equivalent(equivalent(equivalent(B,B),C),D)),equivalent(D,C))).
% 266.02/266.30 173 [hyper,158,1,4] {-} is_a_theorem(equivalent(equivalent(equivalent(A,equivalent(equivalent(B,C),equivalent(equivalent(A,C),B))),equivalent(equivalent(equivalent(D,D),E),F)),equivalent(F,E))).
% 266.02/266.30 174 [hyper,158,1,3] {-} is_a_theorem(equivalent(equivalent(A,B),equivalent(equivalent(equivalent(equivalent(C,D),equivalent(equivalent(equivalent(E,E),D),C)),B),A))).
% 266.02/266.30 175 [hyper,158,1,150] {+} is_a_theorem(equivalent(equivalent(equivalent(A,A),B),B)).
% 266.02/266.30 194 [hyper,158,1,4] {-} is_a_theorem(equivalent(equivalent(equivalent(A,A),equivalent(equivalent(equivalent(B,equivalent(equivalent(C,D),equivalent(equivalent(B,D),C))),E),F)),equivalent(F,E))).
% 266.02/266.30 215 [hyper,165,1,153] {-} is_a_theorem(equivalent(equivalent(equivalent(A,B),equivalent(equivalent(equivalent(equivalent(C,C),D),B),A)),D)).
% 266.02/266.30 222 [hyper,175,1,158] {+} is_a_theorem(equivalent(equivalent(equivalent(A,A),B),equivalent(equivalent(C,C),B))).
% 266.02/266.30 232 [hyper,175,1,3] {-} is_a_theorem(equivalent(equivalent(A,B),equivalent(equivalent(equivalent(equivalent(equivalent(C,C),D),D),B),A))).
% 266.02/266.30 265 [hyper,222,1,175] {+} is_a_theorem(equivalent(equivalent(A,A),equivalent(B,B))).
% 266.02/266.30 324 [hyper,215,1,3] {-} is_a_theorem(equivalent(equivalent(A,B),equivalent(equivalent(equivalent(equivalent(equivalent(C,D),equivalent(equivalent(equivalent(equivalent(E,E),F),D),C)),F),B),A))).
% 266.02/266.30 332 [hyper,265,1,3] {-} is_a_theorem(equivalent(equivalent(A,B),equivalent(equivalent(equivalent(equivalent(C,C),equivalent(D,D)),B),A))).
% 266.02/266.30 476 [hyper,332,1,232] {-} is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,A),equivalent(B,B)),equivalent(equivalent(equivalent(equivalent(equivalent(C,C),D),D),E),F)),equivalent(F,E))).
% 266.02/266.30 507 [hyper,332,1,4] {-} is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,A),equivalent(B,B)),equivalent(equivalent(equivalent(C,equivalent(equivalent(D,E),equivalent(equivalent(C,E),D))),F),G)),equivalent(G,F))).
% 266.02/266.30 546 [hyper,174,1,158] {-} is_a_theorem(equivalent(equivalent(equivalent(A,A),equivalent(equivalent(equivalent(equivalent(B,C),equivalent(equivalent(equivalent(D,D),C),B)),E),F)),equivalent(F,E))).
% 266.02/266.30 567 [hyper,174,1,222] {-} is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,B),equivalent(equivalent(equivalent(C,C),B),A)),equivalent(equivalent(D,D),E)),equivalent(equivalent(F,F),E))).
% 266.02/266.30 5233 [hyper,173,1,165] {-} is_a_theorem(equivalent(A,equivalent(equivalent(equivalent(equivalent(B,B),A),C),C))).
% 266.02/266.30 5302 [hyper,5233,1,3] {-} is_a_theorem(equivalent(equivalent(A,B),equivalent(equivalent(equivalent(C,equivalent(equivalent(equivalent(equivalent(D,D),C),E),E)),B),A))).
% 266.02/266.30 8016 [hyper,324,1,175] {-} is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(A,B),equivalent(equivalent(equivalent(equivalent(C,C),D),B),A)),D),E),E)).
% 266.02/266.30 9434 [hyper,546,1,8016] {-} is_a_theorem(equivalent(A,equivalent(equivalent(equivalent(equivalent(B,B),A),equivalent(equivalent(equivalent(C,C),D),E)),equivalent(E,D)))).
% 266.02/266.30 9666 [hyper,567,1,5302] {-} is_a_theorem(equivalent(equivalent(A,A),equivalent(equivalent(equivalent(equivalent(equivalent(B,B),equivalent(equivalent(C,C),D)),E),E),D))).
% 266.02/266.30 9731 [hyper,9666,1,476] {+} is_a_theorem(equivalent(A,equivalent(equivalent(B,B),A))).
% 266.02/266.30 9735 [hyper,9666,1,194] {-} is_a_theorem(equivalent(A,equivalent(equivalent(B,C),equivalent(equivalent(equivalent(equivalent(D,D),equivalent(equivalent(E,E),A)),C),B)))).
% 266.02/266.30 10046 [hyper,9735,1,158] {-} is_a_theorem(equivalent(equivalent(equivalent(A,A),equivalent(equivalent(B,C),equivalent(equivalent(equivalent(equivalent(D,D),equivalent(equivalent(E,E),F)),C),B))),F)).
% 266.02/266.30 10099 [hyper,9731,1,9434] {-} is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,A),equivalent(B,equivalent(equivalent(C,C),B))),equivalent(equivalent(equivalent(D,D),E),F)),equivalent(F,E))).
% 266.02/266.30 10142 [hyper,9731,1,3] {-} is_a_theorem(equivalent(equivalent(A,B),equivalent(equivalent(equivalent(C,equivalent(equivalent(D,D),C)),B),A))).
% 266.02/266.30 10353 [hyper,10142,1,158] {-} is_a_theorem(equivalent(equivalent(equivalent(A,A),equivalent(equivalent(equivalent(B,equivalent(equivalent(C,C),B)),D),E)),equivalent(E,D))).
% 266.02/266.30 35228 [hyper,10099,1,507] {-} is_a_theorem(equivalent(A,equivalent(equivalent(B,equivalent(equivalent(C,D),equivalent(equivalent(B,D),C))),A))).
% 266.02/266.30 36885 [hyper,35228,1,87] {-} is_a_theorem(equivalent(equivalent(equivalent(A,B),equivalent(equivalent(C,equivalent(equivalent(D,E),equivalent(equivalent(C,E),D))),A)),B)).
% 266.02/266.30 38247 [hyper,36885,1,9731] {-} is_a_theorem(equivalent(equivalent(A,A),equivalent(equivalent(equivalent(B,C),equivalent(equivalent(D,equivalent(equivalent(E,F),equivalent(equivalent(D,F),E))),B)),C))).
% 266.02/266.30 38251 [hyper,36885,1,8016] {-} is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,A),equivalent(equivalent(B,equivalent(equivalent(C,D),equivalent(equivalent(B,D),C))),equivalent(E,F))),F),E)).
% 266.02/266.30 90058 [hyper,38247,1,546] {-} is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,A),B),C),equivalent(equivalent(D,equivalent(equivalent(E,F),equivalent(equivalent(D,F),E))),equivalent(C,B)))).
% 266.02/266.30 90062 [hyper,38251,1,10046] {-} is_a_theorem(equivalent(equivalent(equivalent(A,A),equivalent(equivalent(B,B),C)),equivalent(equivalent(D,E),equivalent(equivalent(C,E),D)))).
% 266.02/266.30 119978 [hyper,90058,1,7] {-} is_a_theorem(equivalent(equivalent(equivalent(A,B),equivalent(equivalent(C,C),A)),B)).
% 266.02/266.30 120171 [hyper,119978,1,9731] {-} is_a_theorem(equivalent(equivalent(A,A),equivalent(equivalent(equivalent(B,C),equivalent(equivalent(D,D),B)),C))).
% 266.02/266.30 120251 [hyper,119978,1,158] {-} is_a_theorem(equivalent(equivalent(equivalent(A,A),B),equivalent(equivalent(C,B),equivalent(equivalent(D,D),C)))).
% 266.02/266.30 120420 [hyper,120171,1,546] {-} is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,A),B),C),equivalent(equivalent(D,D),equivalent(C,B)))).
% 266.02/266.30 120421 [hyper,120171,1,507] {-} is_a_theorem(equivalent(equivalent(equivalent(A,B),equivalent(equivalent(C,B),A)),equivalent(equivalent(D,D),C))).
% 266.02/266.30 120874 [hyper,120251,1,120171] {-} is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(equivalent(B,C),equivalent(equivalent(D,D),B)),C)),equivalent(equivalent(E,E),A))).
% 266.02/266.30 122473 [hyper,120420,1,90062] {-} is_a_theorem(equivalent(equivalent(A,A),equivalent(equivalent(equivalent(B,C),equivalent(equivalent(D,C),B)),equivalent(equivalent(E,E),D)))).
% 266.02/266.30 122880 [hyper,120421,1,119978] {-} is_a_theorem(equivalent(equivalent(equivalent(A,B),B),A)).
% 266.02/266.30 123317 [hyper,122880,1,158] {-} is_a_theorem(equivalent(equivalent(equivalent(A,A),B),equivalent(equivalent(B,C),C))).
% 266.02/266.30 123320 [hyper,122880,1,3] {-} is_a_theorem(equivalent(equivalent(A,B),equivalent(equivalent(equivalent(equivalent(equivalent(C,D),D),C),B),A))).
% 266.02/266.30 135446 [hyper,123320,1,158] {-} is_a_theorem(equivalent(equivalent(equivalent(A,A),equivalent(equivalent(equivalent(equivalent(equivalent(B,C),C),B),D),E)),equivalent(E,D))).
% 266.02/266.30 141032 [hyper,122473,1,10353] {-} is_a_theorem(equivalent(equivalent(equivalent(A,A),B),equivalent(equivalent(B,equivalent(equivalent(C,C),D)),D))).
% 266.02/266.30 141045 [hyper,122473,1,507] {-} is_a_theorem(equivalent(equivalent(equivalent(A,A),B),equivalent(equivalent(B,equivalent(equivalent(C,D),equivalent(equivalent(E,D),C))),E))).
% 266.02/266.30 141054 [hyper,141032,1,120420] {-} is_a_theorem(equivalent(equivalent(A,A),equivalent(equivalent(equivalent(B,equivalent(equivalent(C,C),D)),D),B))).
% 266.02/266.30 141212 [hyper,141054,1,507] {-} is_a_theorem(equivalent(A,equivalent(equivalent(A,B),B))).
% 266.02/266.30 141726 [hyper,141212,1,3] {-} is_a_theorem(equivalent(equivalent(A,B),equivalent(equivalent(equivalent(C,equivalent(equivalent(C,D),D)),B),A))).
% 266.02/266.30 146267 [hyper,141726,1,120874] {-} is_a_theorem(equivalent(equivalent(A,A),equivalent(equivalent(equivalent(B,C),C),equivalent(equivalent(D,D),B)))).
% 266.02/266.30 151377 [hyper,146267,1,123317] {-} is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(A,B),B),equivalent(equivalent(C,C),A)),D),D)).
% 266.02/266.30 151423 [hyper,146267,1,546] {-} is_a_theorem(equivalent(equivalent(equivalent(A,A),equivalent(B,C)),equivalent(equivalent(equivalent(D,D),C),B))).
% 266.02/266.30 151424 [hyper,146267,1,507] {-} is_a_theorem(equivalent(equivalent(equivalent(A,A),B),equivalent(equivalent(C,D),equivalent(equivalent(B,D),C)))).
% 266.02/266.30 151799 [hyper,151423,1,120420] {-} is_a_theorem(equivalent(equivalent(A,A),equivalent(equivalent(equivalent(equivalent(B,B),C),D),equivalent(D,C)))).
% 266.02/266.30 151890 [hyper,151799,1,151377] {-} is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,A),B),C),equivalent(C,B))).
% 266.02/266.30 152005 [hyper,151890,1,151424] {-} is_a_theorem(equivalent(equivalent(equivalent(A,B),equivalent(equivalent(C,B),A)),C)).
% 266.02/266.30 152608 [hyper,152005,1,141212] {-} is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(A,B),equivalent(equivalent(C,B),A)),C),D),D)).
% 266.02/266.30 174715 [hyper,135446,1,122473] {-} is_a_theorem(equivalent(equivalent(equivalent(A,A),B),equivalent(equivalent(B,C),equivalent(equivalent(C,D),D)))).
% 266.02/266.30 175807 [hyper,174715,1,151890] {-} is_a_theorem(equivalent(equivalent(equivalent(A,B),equivalent(equivalent(B,C),C)),A)).
% 266.02/266.30 175826 [hyper,174715,1,120420] {-} is_a_theorem(equivalent(equivalent(A,A),equivalent(equivalent(equivalent(B,C),equivalent(equivalent(C,D),D)),B))).
% 266.02/266.30 176952 [hyper,175826,1,135446] {-} is_a_theorem(equivalent(equivalent(equivalent(A,B),B),equivalent(equivalent(A,C),C))).
% 266.02/266.30 177101 [hyper,176952,1,9731] {-} is_a_theorem(equivalent(equivalent(A,A),equivalent(equivalent(equivalent(B,C),C),equivalent(equivalent(B,D),D)))).
% 266.02/266.30 220935 [hyper,141045,1,151890] {-} is_a_theorem(equivalent(equivalent(equivalent(A,equivalent(equivalent(B,C),equivalent(equivalent(D,C),B))),D),A)).
% 266.02/266.30 221132 [hyper,220935,1,152608] {-} is_a_theorem(equivalent(equivalent(equivalent(A,B),A),B)).
% 266.02/266.30 221671 [hyper,221132,1,9731] {-} is_a_theorem(equivalent(equivalent(A,A),equivalent(equivalent(equivalent(B,C),B),C))).
% 266.02/266.30 221749 [hyper,221132,1,158] {-} is_a_theorem(equivalent(equivalent(equivalent(A,A),B),equivalent(equivalent(C,B),C))).
% 266.02/266.30 221751 [hyper,221132,1,3] {-} is_a_theorem(equivalent(equivalent(A,B),equivalent(equivalent(equivalent(equivalent(equivalent(C,D),C),D),B),A))).
% 266.02/266.30 223281 [hyper,221749,1,221671] {-} is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(equivalent(B,C),B),C)),A)).
% 266.02/266.30 223300 [hyper,221749,1,177101] {-} is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(equivalent(B,C),C),equivalent(equivalent(B,D),D))),A)).
% 266.02/266.30 239194 [hyper,221751,1,223281] {-} is_a_theorem(equivalent(A,equivalent(equivalent(B,A),B))).
% 266.02/266.30 263455 [hyper,223300,1,221751] {-} is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(A,B),A),C),C),B)).
% 266.02/266.30 263628 [hyper,263455,1,239194] {-} is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(equivalent(equivalent(equivalent(B,C),B),D),D),C)),A)).
% 266.02/266.30 263670 [hyper,263455,1,220935] {-} is_a_theorem(equivalent(equivalent(equivalent(A,B),A),equivalent(equivalent(C,D),equivalent(equivalent(B,D),C)))).
% 266.02/266.30 263723 [hyper,263455,1,175807] {-} is_a_theorem(equivalent(equivalent(equivalent(A,equivalent(equivalent(B,C),C)),A),B)).
% 266.02/266.30 264312 [hyper,263723,1,220935] {-} is_a_theorem(equivalent(equivalent(equivalent(A,B),equivalent(equivalent(C,B),A)),equivalent(equivalent(C,D),D))).
% 266.02/266.30 351509 [hyper,264312,1,220935] {-} is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(A,B),B),C),A),C)).
% 266.02/266.30 351540 [hyper,264312,1,36885] {-} is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(A,B),C)),equivalent(C,B))).
% 266.02/266.30 351915 [hyper,351509,1,264312] {-} is_a_theorem(equivalent(equivalent(A,B),equivalent(equivalent(equivalent(A,C),C),B))).
% 266.02/266.30 352431 [hyper,351540,1,263670] {-} is_a_theorem(equivalent(equivalent(equivalent(A,B),equivalent(equivalent(C,A),C)),B)).
% 266.02/266.30 358684 [hyper,352431,1,351540] {-} is_a_theorem(equivalent(equivalent(A,B),equivalent(B,A))).
% 266.02/266.30 359400 [hyper,358684,1,239194] {-} is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,C),equivalent(C,B))),A)).
% 266.02/266.30 359815 [hyper,358684,1,351915] {-} is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,B),B),C),equivalent(A,C))).
% 266.02/266.30 359816 [hyper,358684,1,351540] {-} is_a_theorem(equivalent(equivalent(A,B),equivalent(C,equivalent(equivalent(C,B),A)))).
% 266.02/266.30 380424 [hyper,359400,1,351540] {-} is_a_theorem(equivalent(A,equivalent(equivalent(A,equivalent(B,C)),equivalent(C,B)))).
% 266.02/266.30 388052 [hyper,359816,1,359815] {-} is_a_theorem(equivalent(A,equivalent(B,equivalent(equivalent(B,C),equivalent(A,C))))).
% 266.02/266.30 445566 [hyper,380424,1,263628] {-} is_a_theorem(equivalent(equivalent(equivalent(A,equivalent(B,C)),A),equivalent(C,B))).
% 266.02/266.30 450209 [hyper,388052,1,351540] {-} is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,B),C),equivalent(A,C)),B)).
% 266.02/266.30 491860 [hyper,450209,1,220935] {-} is_a_theorem(equivalent(equivalent(equivalent(A,B),C),equivalent(equivalent(C,B),A))).
% 266.02/266.30 526568 [hyper,491860,1,450209] {-} is_a_theorem(equivalent(equivalent(A,equivalent(B,C)),equivalent(equivalent(B,A),C))).
% 266.02/266.30 526570 [hyper,491860,1,445566] {-} is_a_theorem(equivalent(equivalent(equivalent(A,B),C),equivalent(C,equivalent(B,A)))).
% 266.02/266.30 609996 [hyper,526568,1,526568] {-} is_a_theorem(equivalent(equivalent(equivalent(A,B),equivalent(B,equivalent(A,C))),C)).
% 266.02/266.30 760908 [hyper,609996,1,526570] {-} is_a_theorem(equivalent(A,equivalent(equivalent(B,equivalent(C,A)),equivalent(C,B)))).
% 266.02/266.30 760909 [binary,760908.1,2.1] {-} $F.
% 266.02/266.30
% 266.02/266.30 % SZS output end Refutation
% 266.02/266.30 ------------ end of proof -------------
% 266.02/266.30
% 266.02/266.30
% 266.02/266.30 Search stopped by max_proofs option.
% 266.02/266.30
% 266.02/266.30
% 266.02/266.30 Search stopped by max_proofs option.
% 266.02/266.30
% 266.02/266.30 ============ end of search ============
% 266.02/266.30
% 266.02/266.30 ----------- soft-scott stats ----------
% 266.02/266.30
% 266.02/266.30 true clauses given 1267 (21.2%)
% 266.02/266.30 false clauses given 4713
% 266.02/266.30
% 266.02/266.30 FALSE TRUE
% 266.02/266.30 12 99 4
% 266.02/266.30 16 2401 39
% 266.02/266.30 20 0 485
% 266.02/266.30 24 0 1972
% 266.02/266.30 tot: 2500 2500 (50.0% true)
% 266.02/266.30
% 266.02/266.30
% 266.02/266.30 Model 2 (0.03 seconds, 0 Inserts)
% 266.02/266.30
% 266.02/266.30 That finishes the proof of the theorem.
% 266.02/266.30
% 266.02/266.30 Process 17257 finished Sun Jul 3 18:10:57 2022
%------------------------------------------------------------------------------