%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : MGT047-1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n019.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 22:26:01 EDT 2022
% Result : Unsatisfiable 20.25s 20.46s
% Output : Refutation 20.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : MGT047-1 : TPTP v8.1.0. Released v2.4.0.
% 0.08/0.14 % Command : sos-script %s
% 0.13/0.35 % Computer : n019.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Thu Jun 9 11:39:40 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.13/0.38 ----- Otter 3.2, August 2001 -----
% 0.13/0.38 The process was started by sandbox on n019.cluster.edu,
% 0.13/0.38 Thu Jun 9 11:39:40 2022
% 0.13/0.38 The command was "./sos". The process ID is 4595.
% 0.13/0.38
% 0.13/0.38 set(prolog_style_variables).
% 0.13/0.38 set(auto).
% 0.13/0.38 dependent: set(auto1).
% 0.13/0.38 dependent: set(process_input).
% 0.13/0.38 dependent: clear(print_kept).
% 0.13/0.38 dependent: clear(print_new_demod).
% 0.13/0.38 dependent: clear(print_back_demod).
% 0.13/0.38 dependent: clear(print_back_sub).
% 0.13/0.38 dependent: set(control_memory).
% 0.13/0.38 dependent: assign(max_mem, 12000).
% 0.13/0.38 dependent: assign(pick_given_ratio, 4).
% 0.13/0.38 dependent: assign(stats_level, 1).
% 0.13/0.38 dependent: assign(pick_semantic_ratio, 3).
% 0.13/0.38 dependent: assign(sos_limit, 5000).
% 0.13/0.38 dependent: assign(max_weight, 60).
% 0.13/0.38 clear(print_given).
% 0.13/0.38
% 0.13/0.38 list(usable).
% 0.13/0.38
% 0.13/0.38 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=6.
% 0.13/0.38
% 0.13/0.38 This ia a non-Horn set with equality. The strategy will be
% 0.13/0.38 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.13/0.38 unit deletion, with positive clauses in sos and nonpositive
% 0.13/0.38 clauses in usable.
% 0.13/0.38
% 0.13/0.38 dependent: set(knuth_bendix).
% 0.13/0.38 dependent: set(para_from).
% 0.13/0.38 dependent: set(para_into).
% 0.13/0.38 dependent: clear(para_from_right).
% 0.13/0.38 dependent: clear(para_into_right).
% 0.13/0.38 dependent: set(para_from_vars).
% 0.13/0.38 dependent: set(eq_units_both_ways).
% 0.13/0.38 dependent: set(dynamic_demod_all).
% 0.13/0.38 dependent: set(dynamic_demod).
% 0.13/0.38 dependent: set(order_eq).
% 0.13/0.38 dependent: set(back_demod).
% 0.13/0.38 dependent: set(lrpo).
% 0.13/0.38 dependent: set(hyper_res).
% 0.13/0.38 dependent: set(unit_deletion).
% 0.13/0.38 dependent: set(factor).
% 0.13/0.38
% 0.13/0.38 ------------> process usable:
% 0.13/0.38
% 0.13/0.38 ------------> process sos:
% 0.13/0.38 Following clause subsumed by 41 during input processing: 0 [copy,41,flip.1] {-} A=A.
% 0.13/0.38 41 back subsumes 33.
% 0.13/0.38 41 back subsumes 32.
% 0.13/0.38
% 0.13/0.38 ======= end of input processing =======
% 0.21/0.50
% 0.21/0.50 Model 1 (0.00 seconds, 0 Inserts)
% 0.21/0.50
% 0.21/0.50 Stopped by limit on number of solutions
% 0.21/0.50
% 0.21/0.50
% 0.21/0.50 -------------- Softie stats --------------
% 0.21/0.50
% 0.21/0.50 UPDATE_STOP: 300
% 0.21/0.50 SFINDER_TIME_LIMIT: 2
% 0.21/0.50 SHORT_CLAUSE_CUTOFF: 4
% 0.21/0.50 number of clauses in intial UL: 31
% 0.21/0.50 number of clauses initially in problem: 39
% 0.21/0.50 percentage of clauses intially in UL: 79
% 0.21/0.50 percentage of distinct symbols occuring in initial UL: 100
% 0.21/0.50 percent of all initial clauses that are short: 100
% 0.21/0.50 absolute distinct symbol count: 22
% 0.21/0.50 distinct predicate count: 8
% 0.21/0.50 distinct function count: 8
% 0.21/0.50 distinct constant count: 6
% 0.21/0.50
% 0.21/0.50 ---------- no more Softie stats ----------
% 0.21/0.50
% 0.21/0.50
% 0.21/0.50
% 0.21/0.50 =========== start of search ===========
% 4.26/4.48
% 4.26/4.48
% 4.26/4.48 Changing weight limit from 60 to 42.
% 4.26/4.48
% 4.26/4.48 Stopped by limit on insertions
% 4.26/4.48
% 4.26/4.48 Stopped by limit on insertions
% 4.26/4.48
% 4.26/4.48 Model 2 (0.00 seconds, 0 Inserts)
% 4.26/4.48
% 4.26/4.48 Stopped by limit on number of solutions
% 4.26/4.48
% 4.26/4.48 Stopped by limit on insertions
% 4.26/4.48
% 4.26/4.48 Stopped by limit on insertions
% 4.26/4.48
% 4.26/4.48 Stopped by limit on insertions
% 4.26/4.48
% 4.26/4.48 Stopped by limit on insertions
% 4.26/4.48
% 4.26/4.48 Stopped by limit on insertions
% 4.26/4.48
% 4.26/4.48 Stopped by limit on insertions
% 4.26/4.48
% 4.26/4.48 Stopped by limit on insertions
% 4.26/4.48
% 4.26/4.48 Stopped by limit on insertions
% 4.26/4.48
% 4.26/4.48 Stopped by limit on insertions
% 4.26/4.48
% 4.26/4.48 Stopped by limit on insertions
% 4.26/4.48
% 4.26/4.48 Stopped by limit on insertions
% 4.26/4.48
% 4.26/4.48 Stopped by limit on insertions
% 4.26/4.48
% 4.26/4.48 Stopped by limit on insertions
% 4.26/4.48
% 4.26/4.48 Stopped by limit on insertions
% 4.26/4.48
% 4.26/4.48 Stopped by limit on insertions
% 4.26/4.48
% 4.26/4.48 Stopped by limit on insertions
% 4.26/4.48
% 4.26/4.48 Stopped by limit on insertions
% 4.26/4.48
% 4.26/4.48 Stopped by limit on insertions
% 4.26/4.48
% 4.26/4.48 Stopped by limit on insertions
% 4.26/4.48
% 4.26/4.48 Resetting weight limit to 42 after 85 givens.
% 4.26/4.48
% 4.69/4.95
% 4.69/4.95
% 4.69/4.95 Changing weight limit from 42 to 37.
% 4.69/4.95
% 4.69/4.95 Resetting weight limit to 37 after 90 givens.
% 4.69/4.95
% 6.04/6.29
% 6.04/6.29
% 6.04/6.29 Changing weight limit from 37 to 35.
% 6.04/6.29
% 6.04/6.29 Resetting weight limit to 35 after 100 givens.
% 6.04/6.29
% 8.66/8.85
% 8.66/8.85
% 8.66/8.85 Changing weight limit from 35 to 25.
% 8.66/8.85
% 8.66/8.85 Stopped by limit on insertions
% 8.66/8.85
% 8.66/8.85 Stopped by limit on insertions
% 8.66/8.85
% 8.66/8.85 Stopped by limit on insertions
% 8.66/8.85
% 8.66/8.85 Stopped by limit on insertions
% 8.66/8.85
% 8.66/8.85 Model 3 [ 2 0 2904 ] (0.00 seconds, 250000 Inserts)
% 8.66/8.85
% 8.66/8.85 Stopped by limit on insertions
% 8.66/8.85
% 8.66/8.85 Stopped by limit on insertions
% 8.66/8.85
% 8.66/8.85 Stopped by limit on insertions
% 8.66/8.85
% 8.66/8.85 Resetting weight limit to 25 after 130 givens.
% 8.66/8.85
% 10.71/10.92
% 10.71/10.92
% 10.71/10.92 Changing weight limit from 25 to 20.
% 10.71/10.92
% 10.71/10.92 Stopped by limit on insertions
% 10.71/10.92
% 10.71/10.92 Resetting weight limit to 20 after 235 givens.
% 10.71/10.92
% 10.84/11.03
% 10.84/11.03
% 10.84/11.03 Changing weight limit from 20 to 19.
% 10.84/11.03
% 10.84/11.03 Resetting weight limit to 19 after 240 givens.
% 10.84/11.03
% 11.34/11.58
% 11.34/11.58
% 11.34/11.58 Changing weight limit from 19 to 18.
% 11.34/11.58
% 11.34/11.58 Resetting weight limit to 18 after 260 givens.
% 11.34/11.58
% 11.55/11.74
% 11.55/11.74
% 11.55/11.74 Changing weight limit from 18 to 17.
% 11.55/11.74
% 11.55/11.74 Resetting weight limit to 17 after 265 givens.
% 11.55/11.74
% 14.71/14.95
% 14.71/14.95
% 14.71/14.95 Changing weight limit from 17 to 16.
% 14.71/14.95
% 14.71/14.95 Modelling stopped after 300 given clauses and 0.00 seconds
% 14.71/14.95
% 14.71/14.95
% 14.71/14.95 Resetting weight limit to 16 after 740 givens.
% 14.71/14.95
% 20.25/20.46
% 20.25/20.46 -- HEY sandbox, WE HAVE A PROOF!! --
% 20.25/20.46
% 20.25/20.46 -----> EMPTY CLAUSE at 19.95 sec ----> 29320 [hyper,29283,28623,41] {-} $F.
% 20.25/20.46
% 20.25/20.46 WARNING, clause 11912 not found, proof is incomplete.
% 20.25/20.46 Length of proof is 44. Level of proof is 16.
% 20.25/20.46
% 20.25/20.46 ---------------- PROOF ----------------
% 20.25/20.46 % SZS status Unsatisfiable
% 20.25/20.46 % SZS output start Refutation
% 20.25/20.46
% 20.25/20.46 1 [] {+} -smaller_or_equal(A,B)|smaller(A,B)|A=B.
% 20.25/20.46 2 [] {+} -smaller(A,B)|smaller_or_equal(A,B).
% 20.25/20.46 3 [] {+} A!=B|smaller_or_equal(A,B).
% 20.25/20.46 5 [] {+} -greater(A,B)|greater_or_equal(A,B).
% 20.25/20.46 7 [] {+} -smaller(A,B)|greater(B,A).
% 20.25/20.46 8 [] {+} -greater(A,B)|smaller(B,A).
% 20.25/20.46 9 [] {+} -greater(A,B)| -greater(B,A).
% 20.25/20.46 10 [] {+} -greater(A,B)| -greater(B,C)|greater(A,C).
% 20.25/20.46 12 [] {+} -has_endowment(A)| -smaller_or_equal(age(A,B),eta)|has_immunity(A,B).
% 20.25/20.46 13 [] {+} -has_endowment(A)| -greater(age(A,B),eta)| -has_immunity(A,B).
% 20.25/20.46 17 [] {+} -organization(A)| -has_immunity(A,B)| -has_immunity(A,C)|hazard_of_mortality(A,B)=hazard_of_mortality(A,C).
% 20.25/20.46 18 [] {+} -organization(A)| -has_immunity(A,B)|has_immunity(A,C)|greater(hazard_of_mortality(A,C),hazard_of_mortality(A,B)).
% 20.25/20.46 20 [] {+} -organization(A)|has_immunity(A,B)|has_immunity(A,C)| -greater_or_equal(capability(A,C),capability(A,B))| -greater(position(A,C),position(A,B))|smaller(hazard_of_mortality(A,C),hazard_of_mortality(A,B)).
% 20.25/20.46 22 [] {+} -organization(A)| -greater(stock_of_knowledge(A,B),stock_of_knowledge(A,C))| -smaller_or_equal(internal_friction(A,B),internal_friction(A,C))|greater(capability(A,B),capability(A,C)).
% 20.25/20.46 25 [] {+} -organization(A)| -greater(external_ties(A,B),external_ties(A,C))|greater(position(A,B),position(A,C)).
% 20.25/20.46 27 [] {+} -organization(A)| -greater(age(A,B),age(A,C))|greater(stock_of_knowledge(A,B),stock_of_knowledge(A,C)).
% 20.25/20.46 28 [] {+} -organization(A)| -greater(age(A,B),age(A,C))|greater(external_ties(A,B),external_ties(A,C)).
% 20.25/20.46 29 [] {+} -organization(A)|internal_friction(A,B)=internal_friction(A,C).
% 20.25/20.46 30 [] {+} -greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk6))| -greater(hazard_of_mortality(sk2,sk6),hazard_of_mortality(sk2,sk4))|hazard_of_mortality(sk2,sk4)!=hazard_of_mortality(sk2,sk3).
% 20.25/20.46 31 [factor,9.1.2] {+} -greater(A,A).
% 20.25/20.46 34 [] {+} smaller(A,B)|A=B|greater(A,B).
% 20.25/20.46 35 [] {+} organization(sk2).
% 20.25/20.46 36 [] {-} has_endowment(sk2).
% 20.25/20.46 37 [] {-} smaller_or_equal(age(sk2,sk3),age(sk2,sk4)).
% 20.25/20.46 38 [] {-} smaller_or_equal(age(sk2,sk4),eta).
% 20.25/20.46 39 [] {+} greater(age(sk2,sk5),eta).
% 20.25/20.46 40 [] {-} greater(age(sk2,sk6),age(sk2,sk5)).
% 20.25/20.46 41 [] {+} A=A.
% 20.25/20.46 42 [hyper,34,7] {+} A=B|greater(A,B)|greater(B,A).
% 20.25/20.46 131 [hyper,38,12,36] {-} has_immunity(sk2,sk4).
% 20.25/20.46 151 [hyper,35,29] {+} internal_friction(sk2,A)=internal_friction(sk2,B).
% 20.25/20.46 152 [hyper,35,18,131] {+} has_immunity(sk2,A)|greater(hazard_of_mortality(sk2,A),hazard_of_mortality(sk2,sk4)).
% 20.25/20.46 156 [hyper,37,1,flip.2] {+} smaller(age(sk2,sk3),age(sk2,sk4))|age(sk2,sk4)=age(sk2,sk3).
% 20.25/20.46 175 [hyper,40,28,35] {-} greater(external_ties(sk2,sk6),external_ties(sk2,sk5)).
% 20.25/20.46 176 [hyper,40,27,35] {-} greater(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk5)).
% 20.25/20.46 197 [hyper,175,25,35] {-} greater(position(sk2,sk6),position(sk2,sk5)).
% 20.25/20.46 240 [hyper,39,10,40] {-} greater(age(sk2,sk6),eta).
% 20.25/20.46 318 [hyper,42,13,36,131] {-} age(sk2,sk4)=eta|greater(eta,age(sk2,sk4)).
% 20.25/20.46 368 [para_from,42.1.1,131.1.2] {-} has_immunity(sk2,A)|greater(sk4,A)|greater(A,sk4).
% 20.25/20.46 369 [para_from,42.1.1,38.1.1.2] {-} smaller_or_equal(age(sk2,A),eta)|greater(sk4,A)|greater(A,sk4).
% 20.25/20.46 375 [para_from,42.1.1,197.1.1.2] {-} greater(position(sk2,A),position(sk2,sk5))|greater(sk6,A)|greater(A,sk6).
% 20.25/20.46 409 [para_from,42.1.1,36.1.1] {-} has_endowment(A)|greater(sk2,A)|greater(A,sk2).
% 20.25/20.46 410 [para_from,42.1.1,35.1.1] {+} organization(A)|greater(sk2,A)|greater(A,sk2).
% 20.25/20.46 721 [para_into,240.1.2,42.1.1] {-} greater(age(sk2,sk6),A)|greater(eta,A)|greater(A,eta).
% 20.25/20.46 2219 [hyper,151,3] {+} smaller_or_equal(internal_friction(sk2,A),internal_friction(sk2,B)).
% 20.25/20.46 2734 [hyper,368,17,35,131] {+} greater(sk4,A)|greater(A,sk4)|hazard_of_mortality(sk2,sk4)=hazard_of_mortality(sk2,A).
% 20.25/20.46 7029 [hyper,2219,22,35,176] {-} greater(capability(sk2,sk6),capability(sk2,sk5)).
% 20.25/20.46 7070 [hyper,7029,5] {-} greater_or_equal(capability(sk2,sk6),capability(sk2,sk5)).
% 20.25/20.46 7442 [para_from,318.1.1,37.1.2] {-} smaller_or_equal(age(sk2,sk3),eta)|greater(eta,age(sk2,sk4)).
% 20.25/20.46 7915 [hyper,7442,12,409,unit_del,31,31] {+} greater(eta,age(sk2,sk4))|has_immunity(sk2,sk3).
% 20.25/20.46 9705 [hyper,721,10,721,unit_del,31,31,factor_simp] {-} greater(age(sk2,sk6),A)|greater(A,eta).
% 20.25/20.46 10531 [hyper,152,13,409,9705,unit_del,31,31,31] {-} greater(hazard_of_mortality(sk2,sk6),hazard_of_mortality(sk2,sk4)).
% 20.25/20.46 10534 [hyper,152,13,409,39,unit_del,31,31] {+} greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)).
% 20.25/20.46 10898 [para_from,156.2.1,369.1.1,unit_del,31,31] {-} smaller_or_equal(age(sk2,sk3),eta)|smaller(age(sk2,sk3),age(sk2,sk4)).
% 20.25/20.46 11947 [factor,11912.1.3,unit_del,31,31] {-} -has_immunity(sk2,sk6).
% 20.25/20.46 12030 [para_into,10534.1.2,17.4.1,unit_del,35,131] {+} greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,A))| -has_immunity(sk2,A).
% 20.25/20.46 15735 [hyper,10898,12,409,unit_del,31,31] {+} smaller(age(sk2,sk3),age(sk2,sk4))|has_immunity(sk2,sk3).
% 20.25/20.46 18174 [para_into,12030.1.1,17.4.1,unit_del,35] {-} greater(hazard_of_mortality(sk2,A),hazard_of_mortality(sk2,B))| -has_immunity(sk2,B)| -has_immunity(sk2,sk5)| -has_immunity(sk2,A).
% 20.25/20.46 18194 [factor,18174.2.4,unit_del,31,factor_simp] {+} -has_immunity(sk2,sk5).
% 20.25/20.46 19485 [hyper,375,20,410,7070,unit_del,31,31,18194,11947,31,31] {+} smaller(hazard_of_mortality(sk2,sk6),hazard_of_mortality(sk2,sk5)).
% 20.25/20.46 20098 [hyper,19485,7] {+} greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk6)).
% 20.25/20.46 27324 [hyper,15735,7] {+} has_immunity(sk2,sk3)|greater(age(sk2,sk4),age(sk2,sk3)).
% 20.25/20.46 28593 [para_from,2734.3.1,30.3.1,unit_del,20098,10531] {-} hazard_of_mortality(sk2,A)!=hazard_of_mortality(sk2,sk3)|greater(sk4,A)|greater(A,sk4).
% 20.25/20.46 28597 [factor,28593.2.3,unit_del,31] {-} hazard_of_mortality(sk2,sk4)!=hazard_of_mortality(sk2,sk3).
% 20.25/20.46 28623 [para_into,28597.1.1,17.4.1,unit_del,35,131] {-} hazard_of_mortality(sk2,A)!=hazard_of_mortality(sk2,sk3)| -has_immunity(sk2,A).
% 20.25/20.46 28626 [hyper,28623,41,27324] {-} greater(age(sk2,sk4),age(sk2,sk3)).
% 20.25/20.46 28629 [hyper,28623,41,7915] {-} greater(eta,age(sk2,sk4)).
% 20.25/20.46 28865 [hyper,28626,10,28629] {-} greater(eta,age(sk2,sk3)).
% 20.25/20.46 29063 [hyper,28865,8] {-} smaller(age(sk2,sk3),eta).
% 20.25/20.46 29101 [hyper,29063,2] {-} smaller_or_equal(age(sk2,sk3),eta).
% 20.25/20.46 29283 [hyper,29101,12,409,unit_del,31,31] {+} has_immunity(sk2,sk3).
% 20.25/20.46 29320 [hyper,29283,28623,41] {-} $F.
% 20.25/20.46
% 20.25/20.46 % SZS output end Refutation
% 20.25/20.46 ------------ end of proof -------------
% 20.25/20.46
% 20.25/20.46
% 20.25/20.46 Search stopped by max_proofs option.
% 20.25/20.46
% 20.25/20.46
% 20.25/20.46 Search stopped by max_proofs option.
% 20.25/20.46
% 20.25/20.46 ============ end of search ============
% 20.25/20.46
% 20.25/20.46 ----------- soft-scott stats ----------
% 20.25/20.46
% 20.25/20.46 true clauses given 763 (31.7%)
% 20.25/20.46 false clauses given 1646
% 20.25/20.46
% 20.25/20.46 FALSE TRUE
% 20.25/20.46 5 0 1
% 20.25/20.46 6 0 2
% 20.25/20.46 7 11 1
% 20.25/20.46 9 0 1
% 20.25/20.46 10 3 2
% 20.25/20.46 11 113 166
% 20.25/20.46 12 12 1534
% 20.25/20.46 13 466 558
% 20.25/20.46 14 262 82
% 20.25/20.46 15 694 69
% 20.25/20.46 16 216 108
% 20.25/20.46 tot: 1777 2524 (58.7% true)
% 20.25/20.46
% 20.25/20.46
% 20.25/20.46 Model 3 [ 2 -305 2904 ] (0.00 seconds, 250000 Inserts)
% 20.25/20.46
% 20.25/20.46 That finishes the proof of the theorem.
% 20.25/20.46
% 20.25/20.46 Process 4595 finished Thu Jun 9 11:40:00 2022
%------------------------------------------------------------------------------