%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MSC006-1 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %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 : 300s
% DateTime : Mon Jun 24 11:52:11 EDT 2024
% Result : Unsatisfiable 0.46s 0.62s
% Output : CNFRefutation 0.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : MSC006-1 : TPTP v8.2.0. Released v1.0.0.
% 0.07/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n019.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 : 300
% 0.12/0.34 % DateTime : Sat Jun 22 05:50:54 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.46/0.57 start to proof:theBenchmark
% 0.46/0.61 %-------------------------------------------
% 0.46/0.61 % File :CSE---1.7
% 0.46/0.61 % Problem :theBenchmark
% 0.46/0.61 % Transform :cnf
% 0.46/0.61 % Format :tptp:raw
% 0.46/0.61 % Command :java -jar mcs_scs.jar %d %s
% 0.46/0.61
% 0.46/0.61 % Result :Theorem 0.010000s
% 0.46/0.61 % Output :CNFRefutation 0.010000s
% 0.46/0.61 %-------------------------------------------
% 0.46/0.62 %--------------------------------------------------------------------------
% 0.46/0.62 % File : MSC006-1 : TPTP v8.2.0. Released v1.0.0.
% 0.46/0.62 % Domain : Miscellaneous
% 0.46/0.62 % Problem : A "non-obvious" problem
% 0.46/0.62 % Version : Especial.
% 0.46/0.62 % English : Suppose there are two relations, P and Q. P is transitive, and
% 0.46/0.62 % Q is both transitive and symmetric. Suppose further the
% 0.46/0.62 % "squareness" of P and Q: any two things are related either in
% 0.46/0.62 % the P manner or the Q manner. Prove that either P is total or
% 0.46/0.62 % Q is total.
% 0.46/0.62
% 0.46/0.62 % Refs : [PR86] Pelletier & Rudnicki (1986), Non-Obviousness
% 0.46/0.62 % Source : [PR86]
% 0.46/0.62 % Names : nonob.lop [SETHEO]
% 0.46/0.62
% 0.46/0.62 % Status : Unsatisfiable
% 0.46/0.62 % Rating : 0.00 v2.0.0
% 0.46/0.62 % Syntax : Number of clauses : 6 ( 2 unt; 1 nHn; 5 RR)
% 0.46/0.62 % Number of literals : 12 ( 0 equ; 7 neg)
% 0.46/0.62 % Maximal clause size : 3 ( 2 avg)
% 0.46/0.62 % Maximal term depth : 1 ( 1 avg)
% 0.46/0.62 % Number of predicates : 2 ( 2 usr; 0 prp; 2-2 aty)
% 0.46/0.62 % Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% 0.46/0.62 % Number of variables : 10 ( 0 sgn)
% 0.46/0.62 % SPC : CNF_UNS_EPR_NEQ_NHN
% 0.46/0.62
% 0.46/0.62 % Comments : Rudnicki says "I think that what you call the non-obvious
% 0.46/0.62 % problem from our write-up with Jeff should be attributed
% 0.46/0.62 % to J. \Lo\'{s} (in LaTeX)." and "J. \Lo\'{s} is in LaTeX,
% 0.46/0.62 % and it is the name of my Polish prof that told me that.
% 0.46/0.62 % English approximation of his name can be typed as J. Los.".
% 0.46/0.62 %--------------------------------------------------------------------------
% 0.46/0.62 cnf(p_transitivity,hypothesis,
% 0.46/0.62 ( ~ p(X,Y)
% 0.46/0.62 | ~ p(Y,Z)
% 0.46/0.62 | p(X,Z) ) ).
% 0.46/0.62
% 0.46/0.62 cnf(q_transitivity,hypothesis,
% 0.46/0.62 ( ~ q(X,Y)
% 0.46/0.62 | ~ q(Y,Z)
% 0.46/0.62 | q(X,Z) ) ).
% 0.46/0.62
% 0.46/0.62 cnf(q_symmetry,hypothesis,
% 0.46/0.62 ( ~ q(X,Y)
% 0.46/0.62 | q(Y,X) ) ).
% 0.46/0.62
% 0.46/0.62 cnf(all_related,hypothesis,
% 0.46/0.62 ( p(X,Y)
% 0.46/0.62 | q(X,Y) ) ).
% 0.46/0.62
% 0.46/0.62 cnf(p_is_not_total,hypothesis,
% 0.46/0.62 ~ p(a,b) ).
% 0.46/0.62
% 0.46/0.62 cnf(prove_q_is_total,negated_conjecture,
% 0.46/0.62 ~ q(c,d) ).
% 0.46/0.62
% 0.46/0.62 %--------------------------------------------------------------------------
% 0.46/0.62 %-------------------------------------------
% 0.46/0.62 % Proof found
% 0.46/0.62 % SZS status Theorem for theBenchmark
% 0.46/0.62 % SZS output start Proof
% 0.46/0.62 %ClaNum:6(EqnAxiom:0)
% 0.46/0.62 %VarNum:20(SingletonVarNum:10)
% 0.46/0.62 %MaxLitNum:3
% 0.46/0.62 %MaxfuncDepth:0
% 0.46/0.62 %SharedTerms:6
% 0.46/0.62 %goalClause: 2
% 0.46/0.62 %singleGoalClaCount:1
% 0.46/0.62 [1]~P1(a1,a2)
% 0.46/0.62 [2]~P2(a3,a4)
% 0.46/0.62 [3]P2(x31,x32)+P1(x31,x32)
% 0.46/0.62 [4]~P2(x42,x41)+P2(x41,x42)
% 0.46/0.62 [5]~P1(x51,x53)+P1(x51,x52)+~P1(x53,x52)
% 0.46/0.62 [6]~P2(x61,x63)+P2(x61,x62)+~P2(x63,x62)
% 0.46/0.62 %EqnAxiom
% 0.46/0.62
% 0.46/0.62 %-------------------------------------------
% 0.46/0.63 cnf(11,plain,
% 0.46/0.63 (~P2(x111,a1)+P2(x111,a2)),
% 0.46/0.63 inference(scs_inference,[],[2,1,3,4,6])).
% 0.46/0.63 cnf(13,plain,
% 0.46/0.63 (P2(a2,x131)+~P2(x131,a1)),
% 0.46/0.63 inference(scs_inference,[],[11,4])).
% 0.46/0.63 cnf(15,plain,
% 0.46/0.63 (~P1(a1,x151)+P2(x151,a2)),
% 0.46/0.63 inference(scs_inference,[],[1,5,3])).
% 0.46/0.63 cnf(16,plain,
% 0.46/0.63 (P2(a2,x161)+~P1(a1,x161)),
% 0.46/0.63 inference(scs_inference,[],[15,4])).
% 0.46/0.63 cnf(17,plain,
% 0.46/0.63 (P2(a1,x171)+P2(a2,x171)),
% 0.46/0.63 inference(scs_inference,[],[16,3])).
% 0.46/0.63 cnf(18,plain,
% 0.46/0.63 (P2(x181,a2)+P2(a1,x181)),
% 0.46/0.63 inference(scs_inference,[],[17,4])).
% 0.46/0.63 cnf(19,plain,
% 0.46/0.63 (P2(x191,a1)+P2(x191,a2)),
% 0.46/0.63 inference(scs_inference,[],[18,4])).
% 0.46/0.63 cnf(20,plain,
% 0.46/0.63 (P2(x201,a2)),
% 0.46/0.63 inference(scs_inference,[],[19,11])).
% 0.46/0.63 cnf(23,plain,
% 0.46/0.63 (P2(a2,a1)),
% 0.46/0.63 inference(scs_inference,[],[1,3,4])).
% 0.46/0.63 cnf(26,plain,
% 0.46/0.63 (P2(a2,x261)),
% 0.46/0.63 inference(scs_inference,[],[23,20,6,13])).
% 0.46/0.63 cnf(29,plain,
% 0.46/0.63 ($false),
% 0.46/0.63 inference(scs_inference,[],[20,2,26,6]),
% 0.46/0.63 ['proof']).
% 0.46/0.63 % SZS output end Proof
% 0.46/0.63 % Total time :0.010000s
%------------------------------------------------------------------------------