%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : PUZ005-1 : TPTP v8.1.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n032.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 : Mon Jul 18 18:26:57 EDT 2022
% Result : Unsatisfiable 1.05s 1.25s
% Output : Refutation 1.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.09 % Problem : PUZ005-1 : TPTP v8.1.0. Released v1.0.0.
% 0.08/0.10 % Command : sos-script %s
% 0.10/0.29 % Computer : n032.cluster.edu
% 0.10/0.29 % Model : x86_64 x86_64
% 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.29 % Memory : 8042.1875MB
% 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.29 % CPULimit : 300
% 0.10/0.29 % WCLimit : 600
% 0.10/0.29 % DateTime : Sat May 28 21:17:40 EDT 2022
% 0.10/0.29 % CPUTime :
% 0.10/0.30 ----- Otter 3.2, August 2001 -----
% 0.10/0.30 The process was started by sandbox2 on n032.cluster.edu,
% 0.10/0.30 Sat May 28 21:17:40 2022
% 0.10/0.30 The command was "./sos". The process ID is 9714.
% 0.10/0.30
% 0.10/0.30 set(prolog_style_variables).
% 0.10/0.30 set(auto).
% 0.10/0.30 dependent: set(auto1).
% 0.10/0.30 dependent: set(process_input).
% 0.10/0.30 dependent: clear(print_kept).
% 0.10/0.30 dependent: clear(print_new_demod).
% 0.10/0.30 dependent: clear(print_back_demod).
% 0.10/0.30 dependent: clear(print_back_sub).
% 0.10/0.30 dependent: set(control_memory).
% 0.10/0.30 dependent: assign(max_mem, 12000).
% 0.10/0.30 dependent: assign(pick_given_ratio, 4).
% 0.10/0.30 dependent: assign(stats_level, 1).
% 0.10/0.30 dependent: assign(pick_semantic_ratio, 3).
% 0.10/0.30 dependent: assign(sos_limit, 5000).
% 0.10/0.30 dependent: assign(max_weight, 60).
% 0.10/0.30 clear(print_given).
% 0.10/0.30
% 0.10/0.30 list(usable).
% 0.10/0.30
% 0.10/0.30 SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=7.
% 0.10/0.30
% 0.10/0.30 This is a non-Horn set without equality. The strategy
% 0.10/0.30 will be ordered hyper_res, ur_res, unit deletion, and
% 0.10/0.30 factoring, with satellites in sos and nuclei in usable.
% 0.10/0.30
% 0.10/0.30 dependent: set(hyper_res).
% 0.10/0.30 dependent: set(factor).
% 0.10/0.30 dependent: set(unit_deletion).
% 0.10/0.30
% 0.10/0.30 ------------> process usable:
% 0.10/0.30
% 0.10/0.30 ------------> process sos:
% 0.10/0.30
% 0.10/0.30 ======= end of input processing =======
% 0.14/0.33
% 0.14/0.33 Model 1 (0.00 seconds, 0 Inserts)
% 0.14/0.33
% 0.14/0.33 Stopped by limit on number of solutions
% 0.14/0.33
% 0.14/0.33
% 0.14/0.33 -------------- Softie stats --------------
% 0.14/0.33
% 0.14/0.33 UPDATE_STOP: 300
% 0.14/0.33 SFINDER_TIME_LIMIT: 2
% 0.14/0.33 SHORT_CLAUSE_CUTOFF: 4
% 0.14/0.33 number of clauses in intial UL: 50
% 0.14/0.33 number of clauses initially in problem: 53
% 0.14/0.33 percentage of clauses intially in UL: 94
% 0.14/0.33 percentage of distinct symbols occuring in initial UL: 100
% 0.14/0.33 percent of all initial clauses that are short: 100
% 0.14/0.33 absolute distinct symbol count: 14
% 0.14/0.33 distinct predicate count: 9
% 0.14/0.33 distinct function count: 2
% 0.14/0.33 distinct constant count: 3
% 0.14/0.33
% 0.14/0.33 ---------- no more Softie stats ----------
% 0.14/0.33
% 0.14/0.33
% 0.14/0.33
% 0.14/0.33 =========== start of search ===========
% 1.05/1.25
% 1.05/1.25 -------- PROOF --------
% 1.05/1.25 % SZS status Unsatisfiable
% 1.05/1.25 % SZS output start Refutation
% 1.05/1.25
% 1.05/1.25 -----> EMPTY CLAUSE at 0.94 sec ----> 256 [hyper,251,46,174,187] {-} $F.
% 1.05/1.25
% 1.05/1.25 Length of proof is 34. Level of proof is 17.
% 1.05/1.25
% 1.05/1.25 ---------------- PROOF ----------------
% 1.05/1.25 % SZS status Unsatisfiable
% 1.05/1.25 % SZS output start Refutation
% 1.05/1.25
% 1.05/1.25 6 [] {+} -monday(A)| -sunday(A).
% 1.05/1.25 11 [] {+} -tuesday(A)| -sunday(A).
% 1.05/1.25 15 [] {+} -wednesday(A)| -sunday(A).
% 1.05/1.25 22 [] {+} -monday(yesterday(A))|tuesday(A).
% 1.05/1.25 23 [] {+} -tuesday(yesterday(A))|wednesday(A).
% 1.05/1.25 24 [] {+} -wednesday(yesterday(A))|thursday(A).
% 1.05/1.25 25 [] {+} -thursday(yesterday(A))|friday(A).
% 1.05/1.25 26 [] {+} -friday(yesterday(A))|saturday(A).
% 1.05/1.25 27 [] {+} -saturday(yesterday(A))|sunday(A).
% 1.05/1.25 32 [] {+} thursday(yesterday(A))| -friday(A).
% 1.05/1.25 33 [] {+} friday(yesterday(A))| -saturday(A).
% 1.05/1.25 36 [] {+} -member(A,lying_days(lion))|monday(A)|tuesday(A)|wednesday(A).
% 1.05/1.25 37 [] {+} -member(A,lying_days(unicorn))|thursday(A)|friday(A)|saturday(A).
% 1.05/1.25 39 [] {+} -tuesday(A)|member(A,lying_days(lion)).
% 1.05/1.25 40 [] {+} -wednesday(A)|member(A,lying_days(lion)).
% 1.05/1.25 41 [] {+} -thursday(A)|member(A,lying_days(unicorn)).
% 1.05/1.25 42 [] {+} -friday(A)|member(A,lying_days(unicorn)).
% 1.05/1.25 43 [] {+} -saturday(A)|member(A,lying_days(unicorn)).
% 1.05/1.25 44 [] {+} member(A,lying_days(B))| -admits(B,A,C)|member(C,lying_days(B)).
% 1.05/1.25 45 [] {+} member(A,lying_days(B))|admits(B,A,C)| -member(C,lying_days(B)).
% 1.05/1.25 46 [] {+} -member(A,lying_days(B))| -admits(B,A,C)| -member(C,lying_days(B)).
% 1.05/1.25 47 [] {+} -member(A,lying_days(B))|admits(B,A,C)|member(C,lying_days(B)).
% 1.05/1.25 48 [] {+} -thursday(today).
% 1.05/1.25 52 [] {-} admits(lion,today,yesterday(today)).
% 1.05/1.25 53 [] {-} admits(unicorn,today,yesterday(today)).
% 1.05/1.25 57 [hyper,52,44] {-} member(today,lying_days(lion))|member(yesterday(today),lying_days(lion)).
% 1.05/1.25 58 [hyper,53,44] {-} member(today,lying_days(unicorn))|member(yesterday(today),lying_days(unicorn)).
% 1.05/1.25 64 [hyper,57,36] {-} member(today,lying_days(lion))|monday(yesterday(today))|tuesday(yesterday(today))|wednesday(yesterday(today)).
% 1.05/1.25 68 [hyper,58,45] {-} member(yesterday(today),lying_days(unicorn))|member(A,lying_days(unicorn))|admits(unicorn,A,today).
% 1.05/1.25 69 [hyper,58,37,unit_del,48] {-} member(yesterday(today),lying_days(unicorn))|friday(today)|saturday(today).
% 1.05/1.25 70 [hyper,58,47] {-} member(today,lying_days(unicorn))|admits(unicorn,yesterday(today),A)|member(A,lying_days(unicorn)).
% 1.05/1.25 73 [factor,68.1.2] {-} member(yesterday(today),lying_days(unicorn))|admits(unicorn,yesterday(today),today).
% 1.05/1.25 74 [factor,70.1.3] {-} member(today,lying_days(unicorn))|admits(unicorn,yesterday(today),today).
% 1.05/1.25 79 [hyper,69,33] {-} member(yesterday(today),lying_days(unicorn))|friday(today)|friday(yesterday(today)).
% 1.05/1.25 91 [hyper,73,46,74,53,factor_simp] {-} admits(unicorn,yesterday(today),today).
% 1.05/1.25 95 [hyper,79,42,factor_simp] {-} member(yesterday(today),lying_days(unicorn))|friday(today).
% 1.05/1.25 96 [hyper,95,32] {-} member(yesterday(today),lying_days(unicorn))|thursday(yesterday(today)).
% 1.05/1.25 97 [hyper,96,41,factor_simp] {-} member(yesterday(today),lying_days(unicorn)).
% 1.05/1.25 100 [hyper,97,37] {-} thursday(yesterday(today))|friday(yesterday(today))|saturday(yesterday(today)).
% 1.05/1.25 118 [hyper,100,25] {-} friday(yesterday(today))|saturday(yesterday(today))|friday(today).
% 1.05/1.25 119 [hyper,118,33] {-} friday(yesterday(today))|friday(today)|friday(yesterday(yesterday(today))).
% 1.05/1.25 132 [hyper,119,26] {-} friday(today)|friday(yesterday(yesterday(today)))|saturday(today).
% 1.05/1.25 137 [hyper,132,43] {-} friday(today)|friday(yesterday(yesterday(today)))|member(today,lying_days(unicorn)).
% 1.05/1.25 149 [hyper,137,42,factor_simp] {-} friday(yesterday(yesterday(today)))|member(today,lying_days(unicorn)).
% 1.05/1.25 159 [hyper,149,42] {-} member(today,lying_days(unicorn))|member(yesterday(yesterday(today)),lying_days(unicorn)).
% 1.05/1.25 161 [hyper,149,26] {-} member(today,lying_days(unicorn))|saturday(yesterday(today)).
% 1.05/1.25 162 [hyper,161,27] {-} member(today,lying_days(unicorn))|sunday(today).
% 1.05/1.25 174 [hyper,159,46,97,91] {-} member(yesterday(yesterday(today)),lying_days(unicorn)).
% 1.05/1.25 179 [hyper,174,47] {-} admits(unicorn,yesterday(yesterday(today)),A)|member(A,lying_days(unicorn)).
% 1.05/1.25 187 [hyper,179,46,97,91] {-} admits(unicorn,yesterday(yesterday(today)),today).
% 1.05/1.25 191 [hyper,64,24,unit_del,48] {-} member(today,lying_days(lion))|monday(yesterday(today))|tuesday(yesterday(today)).
% 1.05/1.25 200 [hyper,191,23] {-} member(today,lying_days(lion))|monday(yesterday(today))|wednesday(today).
% 1.05/1.25 210 [hyper,200,40,factor_simp] {-} member(today,lying_days(lion))|monday(yesterday(today)).
% 1.05/1.25 212 [hyper,210,22] {-} member(today,lying_days(lion))|tuesday(today).
% 1.05/1.25 218 [hyper,212,39,factor_simp] {-} member(today,lying_days(lion)).
% 1.05/1.25 221 [hyper,218,36] {-} monday(today)|tuesday(today)|wednesday(today).
% 1.05/1.25 226 [hyper,221,15,162] {-} monday(today)|tuesday(today)|member(today,lying_days(unicorn)).
% 1.05/1.25 249 [hyper,226,11,162,factor_simp] {-} monday(today)|member(today,lying_days(unicorn)).
% 1.05/1.25 251 [hyper,249,6,162,factor_simp] {-} member(today,lying_days(unicorn)).
% 1.05/1.25 256 [hyper,251,46,174,187] {-} $F.
% 1.05/1.25
% 1.05/1.25 % SZS output end Refutation
% 1.05/1.25 ------------ end of proof -------------
% 1.05/1.25
% 1.05/1.25
% 1.05/1.25 Search stopped by max_proofs option.
% 1.05/1.25
% 1.05/1.25
% 1.05/1.25 Search stopped by max_proofs option.
% 1.05/1.25
% 1.05/1.26 ============ end of search ============
% 1.05/1.26
% 1.05/1.26 ----------- soft-scott stats ----------
% 1.05/1.26
% 1.05/1.26 true clauses given 0 (0.0%)
% 1.05/1.26 false clauses given 64
% 1.05/1.26
% 1.05/1.26 FALSE TRUE
% 1.05/1.26 8 2 0
% 1.05/1.26 9 2 0
% 1.05/1.26 10 5 0
% 1.05/1.26 11 8 0
% 1.05/1.26 12 10 0
% 1.05/1.26 13 4 0
% 1.05/1.26 14 4 0
% 1.05/1.26 15 2 0
% 1.05/1.26 16 2 0
% 1.05/1.26 17 2 0
% 1.05/1.26 18 1 0
% 1.05/1.26 19 2 0
% 1.05/1.26 21 1 0
% 1.05/1.26 23 1 0
% 1.05/1.26 27 1 0
% 1.05/1.26 37 1 0
% 1.05/1.26 42 1 0
% 1.05/1.26 tot: 49 0 (0.0% true)
% 1.05/1.26
% 1.05/1.26
% 1.05/1.26 Model 1 (0.00 seconds, 0 Inserts)
% 1.05/1.26
% 1.05/1.26 That finishes the proof of the theorem.
% 1.05/1.26
% 1.05/1.26 Process 9714 finished Sat May 28 21:17:41 2022
%------------------------------------------------------------------------------