%------------------------------------------------------------------------------
% File : LisaTT---0.9.1
% Problem : MGT115+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -cp /export/starexec/sandbox2/solver/bin/lisa-assembly-0.9.jar TPTP_Lisa tableau --input /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n029.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 : Wed Apr 29 02:09:06 PM UTC 2026
% Result : Theorem 1.71s 1.15s
% Output : Proof 1.71s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(issue_injective,axiom,
! [A,B] :
( issue(A) = issue(B)
=> A = B ) ).
fof(rule_pi1,axiom,
rule(pi1) ).
fof(rule_pi2,axiom,
rule(pi2) ).
fof(pi1_neq_pi2,axiom,
pi1 != pi2 ).
fof(s0,plain,
( [ issue(pi2) = issue(pi1),issue(pi2) != issue(pi1) ]
--> [ ] ),
inference(restate_true,[status(thm)],[]) ).
fof(s1,plain,
( [ pi2 = pi1,pi2 != pi1 ]
--> [ ] ),
inference(restate_true,[status(thm)],[]) ).
fof(s2,plain,
( [ issue(pi2) = issue(pi1),pi2 != pi1,
( issue(pi2) != issue(pi1)
| pi2 = pi1 ) ]
--> [ ] ),
inference(left_or,[status(thm)],[s0,s1]) ).
fof(s3,plain,
( [ issue(pi2) = issue(pi1),pi2 != pi1,
! [B] :
( issue(B) != issue(pi1)
| B = pi1 ) ]
--> [ ] ),
inference(left_forall,[status(thm)],[s2]) ).
fof(s4,plain,
( [ issue(pi2) = issue(pi1),pi2 != pi1,
! [A,B] :
( issue(B) != issue(A)
| B = A ) ]
--> [ ] ),
inference(left_forall,[status(thm)],[s3]) ).
fof(s5,plain,
( [ issue(pi2) = issue(pi1),
! [A,B] :
( issue(B) != issue(A)
| B = A ),
( pi2 != pi1
& rule(pi1) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s4]) ).
fof(s6,plain,
( [ issue(pi2) = issue(pi1),
( pi2 != pi1
& rule(pi1)
& ! [A,B] :
( issue(B) != issue(A)
| B = A ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s5]) ).
fof(s7,plain,
( [ issue(pi2) = issue(pi1),
( pi2 != pi1
& rule(pi1)
& ! [A,B] :
( issue(B) != issue(A)
| B = A )
& rule(pi2) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s6]) ).
fof(s8,plain,
( [ ( pi2 != pi1
& rule(pi1)
& ! [A,B] :
( issue(B) != issue(A)
| B = A )
& rule(pi2)
& issue(pi2) = issue(pi1) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s7]) ).
fof(s9,plain,
( [ ( pi2 != pi1
& rule(pi1)
& ! [A,B] :
( issue(B) != issue(A)
| B = A )
& rule(pi2)
& issue(pi2) = issue(pi1) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s8]) ).
fof(s10,plain,
( [ ! [A,B] :
( issue(A) = issue(B)
=> A = B ),
rule(pi1),rule(pi2),pi1 != pi2 ]
--> [ issue(pi1) != issue(pi2) ] ),
inference(restate,[status(thm)],[s9]) ).
fof(final,theorem,
issue(pi1) != issue(pi2),
inference(big_cut,[status(thm)],[issue_injective,rule_pi1,rule_pi2,pi1_neq_pi2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : MGT115+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : java -cp /export/starexec/sandbox2/solver/bin/lisa-assembly-0.9.jar TPTP_Lisa tableau --input /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.33 % Computer : n029.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue Apr 28 19:31:59 EDT 2026
% 0.15/0.33 % CPUTime :
% 1.71/1.15 % SZS status Theorem
% 1.71/1.17 % SZS output start Proof
% See solution above
%------------------------------------------------------------------------------