%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : COL099-2 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 08:14:34 AM UTC 2026
% Result : Unsatisfiable 12.16s 12.42s
% Output : Proof 12.25s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause1,axiom,
member(U,cons(U,V)),
file('theBenchmark.p',clause1) ).
cnf(clause2,axiom,
( member(U,cons(W,V))
| ~ member(U,V) ),
file('theBenchmark.p',clause2) ).
cnf(clause3,axiom,
( member(succ(U),nat)
| ~ member(U,nat) ),
file('theBenchmark.p',clause3) ).
cnf(clause4,axiom,
( inr(U) = inr(V)
| U != V ),
file('theBenchmark.p',clause4) ).
cnf(clause5,axiom,
( inl(U) = inl(V)
| U != V ),
file('theBenchmark.p',clause5) ).
cnf(clause6,axiom,
( member(inl(U),disjsum(V,W))
| ~ member(U,V) ),
file('theBenchmark.p',clause6) ).
cnf(clause7,axiom,
( member(inr(U),disjsum(W,V))
| ~ member(U,V) ),
file('theBenchmark.p',clause7) ).
cnf(clause8,axiom,
( member(W,V)
| member(cons_subsetI_sk1(U,X,V),X)
| ~ member(W,cons(U,X))
| ~ member(U,V) ),
file('theBenchmark.p',clause8) ).
cnf(clause9,axiom,
( member(X,V)
| ~ member(X,cons(U,W))
| ~ member(cons_subsetI_sk1(U,W,V),V)
| ~ member(U,V) ),
file('theBenchmark.p',clause9) ).
cnf(clause9_1,axiom,
( subset(cons(A,B),C)
| ~ subset(B,C)
| ~ member(A,C) ),
file('theBenchmark.p',clause9_1) ).
cnf(clause10,axiom,
( member(pair(V,U),converse(W))
| ~ member(pair(U,V),W) ),
file('theBenchmark.p',clause10) ).
cnf(clause11,axiom,
( cons(U,eptset) = cons(V,eptset)
| U != V ),
file('theBenchmark.p',clause11) ).
cnf(clause12,axiom,
( member(U,succ(V))
| ~ member(U,V) ),
file('theBenchmark.p',clause12) ).
cnf(clause13,axiom,
( member(U,succ(V))
| U != V ),
file('theBenchmark.p',clause13) ).
cnf(clause14,axiom,
member(U,cons(U,eptset)),
file('theBenchmark.p',clause14) ).
cnf(clause15,axiom,
( member(U,cons(W,V))
| ~ member(U,V) ),
file('theBenchmark.p',clause15) ).
cnf(clause16,axiom,
( member(U,cons(V,W))
| U != V ),
file('theBenchmark.p',clause16) ).
cnf(clause17,axiom,
( member(U,diff(V,W))
| member(U,W)
| ~ member(U,V) ),
file('theBenchmark.p',clause17) ).
cnf(clause18,axiom,
( member(U,int(V,W))
| ~ member(U,W)
| ~ member(U,V) ),
file('theBenchmark.p',clause18) ).
cnf(clause19,axiom,
( member(U,un(W,V))
| ~ member(U,V) ),
file('theBenchmark.p',clause19) ).
cnf(clause20,axiom,
( member(U,un(V,W))
| ~ member(U,V) ),
file('theBenchmark.p',clause20) ).
cnf(clause21,axiom,
( member(U,pow(V))
| member(powI_sk1(U,V),U) ),
file('theBenchmark.p',clause21) ).
cnf(clause22,axiom,
( member(U,pow(V))
| ~ member(powI_sk1(U,V),V) ),
file('theBenchmark.p',clause22) ).
cnf(clause23,axiom,
( member(W,inter(V))
| member(interI_sk1(W,V),V)
| ~ member(U,V) ),
file('theBenchmark.p',clause23) ).
cnf(clause24,axiom,
( member(U,inter(V))
| ~ member(W,V)
| ~ member(U,interI_sk1(U,V)) ),
file('theBenchmark.p',clause24) ).
cnf(clause25,axiom,
( card(union(U))
| member(card_Union_sk1(U),U) ),
file('theBenchmark.p',clause25) ).
cnf(clause26,axiom,
( card(union(U))
| ~ card(card_Union_sk1(U)) ),
file('theBenchmark.p',clause26) ).
cnf(clause27,axiom,
( member(int(U,W),fin(V))
| ~ member(U,fin(V)) ),
file('theBenchmark.p',clause27) ).
cnf(clause28,axiom,
( member(int(W,U),fin(V))
| ~ member(U,fin(V)) ),
file('theBenchmark.p',clause28) ).
cnf(clause29,axiom,
( ord(inter(U))
| member(order_Inter_sk1(U),U) ),
file('theBenchmark.p',clause29) ).
cnf(clause30,axiom,
( ord(inter(U))
| ~ ord(order_Inter_sk1(U)) ),
file('theBenchmark.p',clause30) ).
cnf(clause31,axiom,
( ord(union(U))
| member(order_Union_sk1(U),U) ),
file('theBenchmark.p',clause31) ).
cnf(clause32,axiom,
( ord(union(U))
| ~ ord(order_Union_sk1(U)) ),
file('theBenchmark.p',clause32) ).
cnf(clause33,axiom,
( ord(un(U,V))
| ~ ord(V)
| ~ ord(U) ),
file('theBenchmark.p',clause33) ).
cnf(clause34,axiom,
( member(pair(U,X),comp(Y,W))
| ~ member(pair(V,X),Y)
| ~ member(pair(U,V),W) ),
file('theBenchmark.p',clause34) ).
cnf(clause35,axiom,
( member(U,vimage(W,X))
| ~ member(V,X)
| ~ member(pair(U,V),W) ),
file('theBenchmark.p',clause35) ).
cnf(clause36,axiom,
( member(V,image(W,X))
| ~ member(U,X)
| ~ member(pair(U,V),W) ),
file('theBenchmark.p',clause36) ).
cnf(clause37,axiom,
qInr(U) != qInl(V),
file('theBenchmark.p',clause37) ).
cnf(clause38,axiom,
qInl(U) != qInr(V),
file('theBenchmark.p',clause38) ).
cnf(clause39,axiom,
( U = V
| qInr(U) != qInr(V) ),
file('theBenchmark.p',clause39) ).
cnf(clause40,axiom,
( U = V
| qInl(U) != qInl(V) ),
file('theBenchmark.p',clause40) ).
cnf(clause41,axiom,
( member(qsumE_sk2(U,V,W),W)
| member(qsumE_sk1(U,V,W),V)
| ~ member(U,qsum(V,W)) ),
file('theBenchmark.p',clause41) ).
cnf(clause42,axiom,
( U = qInr(qsumE_sk2(U,V,W))
| member(qsumE_sk1(U,V,W),V)
| ~ member(U,qsum(V,W)) ),
file('theBenchmark.p',clause42) ).
cnf(clause43,axiom,
( member(qsumE_sk2(U,V,W),W)
| U = qInl(qsumE_sk1(U,V,W))
| ~ member(U,qsum(V,W)) ),
file('theBenchmark.p',clause43) ).
cnf(clause44,axiom,
( U = qInr(qsumE_sk2(U,V,W))
| U = qInl(qsumE_sk1(U,V,W))
| ~ member(U,qsum(V,W)) ),
file('theBenchmark.p',clause44) ).
cnf(clause45,axiom,
( U = qPair(qconverseE_sk2(U,V),qconverseE_sk1(U,V))
| ~ member(U,qconverse(V)) ),
file('theBenchmark.p',clause45) ).
cnf(clause46,axiom,
( member(qPair(qconverseE_sk1(U,V),qconverseE_sk2(U,V)),V)
| ~ member(U,qconverse(V)) ),
file('theBenchmark.p',clause46) ).
cnf(clause47,axiom,
( member(qPair(V,U),W)
| ~ member(qPair(U,V),qconverse(W)) ),
file('theBenchmark.p',clause47) ).
cnf(clause48,axiom,
( U = W
| qPair(U,V) != qPair(W,X) ),
file('theBenchmark.p',clause48) ).
cnf(clause49,axiom,
( V = X
| qPair(U,V) != qPair(W,X) ),
file('theBenchmark.p',clause49) ).
cnf(clause50,axiom,
( member(U,nat)
| ~ member(succ(U),nat) ),
file('theBenchmark.p',clause50) ).
cnf(clause51,axiom,
( rmultE_c2(U,V,W,X,Y,Z,X1,X2)
| rmultE_c1(U,V,W,X,Y,Z,X1,X2)
| ~ member(pair(pair(U,V),pair(W,X)),rmult(Y,Z,X1,X2)) ),
file('theBenchmark.p',clause51) ).
cnf(clause52,axiom,
( member(pair(U,W),Z)
| ~ rmultE_c1(U,V,W,X,Y,Z,X1,X2) ),
file('theBenchmark.p',clause52) ).
cnf(clause53,axiom,
( member(U,Y)
| ~ rmultE_c1(U,V,W,X,Y,Z,X1,X2) ),
file('theBenchmark.p',clause53) ).
cnf(clause54,axiom,
( member(W,Y)
| ~ rmultE_c1(U,V,W,X,Y,Z,X1,X2) ),
file('theBenchmark.p',clause54) ).
cnf(clause55,axiom,
( member(V,X1)
| ~ rmultE_c1(U,V,W,X,Y,Z,X1,X2) ),
file('theBenchmark.p',clause55) ).
cnf(clause56,axiom,
( member(X,X1)
| ~ rmultE_c1(U,V,W,X,Y,Z,X1,X2) ),
file('theBenchmark.p',clause56) ).
cnf(clause57,axiom,
( member(pair(V,X),X2)
| ~ rmultE_c2(U,V,W,X,Y,Z,X1,X2) ),
file('theBenchmark.p',clause57) ).
cnf(clause58,axiom,
( member(W,Y)
| ~ rmultE_c2(U,V,W,X,Y,Z,X1,X2) ),
file('theBenchmark.p',clause58) ).
cnf(clause59,axiom,
( U = W
| ~ rmultE_c2(U,V,W,X,Y,Z,X1,X2) ),
file('theBenchmark.p',clause59) ).
cnf(clause60,axiom,
( member(V,X1)
| ~ rmultE_c2(U,V,W,X,Y,Z,X1,X2) ),
file('theBenchmark.p',clause60) ).
cnf(clause61,axiom,
( member(X,X1)
| ~ rmultE_c2(U,V,W,X,Y,Z,X1,X2) ),
file('theBenchmark.p',clause61) ).
cnf(clause62,axiom,
~ member(pair(inr(U),inl(V)),radd(W,X,Y,Z)),
file('theBenchmark.p',clause62) ).
cnf(clause63,axiom,
( member(U,Y)
| ~ member(pair(inr(U),inr(V)),radd(W,X,Y,Z)) ),
file('theBenchmark.p',clause63) ).
cnf(clause64,axiom,
( member(V,Y)
| ~ member(pair(inr(U),inr(V)),radd(W,X,Y,Z)) ),
file('theBenchmark.p',clause64) ).
cnf(clause65,axiom,
( member(pair(U,V),Z)
| ~ member(pair(inr(U),inr(V)),radd(W,X,Y,Z)) ),
file('theBenchmark.p',clause65) ).
cnf(clause66,axiom,
( member(U,W)
| ~ member(pair(inl(U),inl(V)),radd(W,X,Y,Z)) ),
file('theBenchmark.p',clause66) ).
cnf(clause67,axiom,
( member(V,W)
| ~ member(pair(inl(U),inl(V)),radd(W,X,Y,Z)) ),
file('theBenchmark.p',clause67) ).
cnf(clause68,axiom,
( member(pair(U,V),X)
| ~ member(pair(inl(U),inl(V)),radd(W,X,Y,Z)) ),
file('theBenchmark.p',clause68) ).
cnf(clause69,axiom,
( member(U,W)
| ~ member(pair(inl(U),inr(V)),radd(W,X,Y,Z)) ),
file('theBenchmark.p',clause69) ).
cnf(clause70,axiom,
( member(V,Y)
| ~ member(pair(inl(U),inr(V)),radd(W,X,Y,Z)) ),
file('theBenchmark.p',clause70) ).
cnf(clause71,axiom,
( lt(U,V)
| ~ le(succ(U),V) ),
file('theBenchmark.p',clause71) ).
cnf(clause72,axiom,
( ord(U)
| ~ le(eptset,succ(U)) ),
file('theBenchmark.p',clause72) ).
cnf(clause73,axiom,
( member(U,W)
| ~ member(pair(U,V),memrel(W)) ),
file('theBenchmark.p',clause73) ).
cnf(clause74,axiom,
( member(V,W)
| ~ member(pair(U,V),memrel(W)) ),
file('theBenchmark.p',clause74) ).
cnf(clause75,axiom,
( member(U,V)
| ~ member(pair(U,V),memrel(W)) ),
file('theBenchmark.p',clause75) ).
cnf(clause76,axiom,
( U = eptset
| ~ le(U,eptset) ),
file('theBenchmark.p',clause76) ).
cnf(clause77,axiom,
( ord(U)
| ~ le(U,U) ),
file('theBenchmark.p',clause77) ).
cnf(clause78,axiom,
( ord(U)
| ~ ord(succ(U)) ),
file('theBenchmark.p',clause78) ).
cnf(clause79,axiom,
( U = pair(compE_sk1(U,V,W),compE_sk3(U,V,W))
| ~ member(U,comp(V,W)) ),
file('theBenchmark.p',clause79) ).
cnf(clause80,axiom,
( member(pair(compE_sk1(U,V,W),compE_sk2(U,V,W)),W)
| ~ member(U,comp(V,W)) ),
file('theBenchmark.p',clause80) ).
cnf(clause81,axiom,
( member(pair(compE_sk2(U,V,W),compE_sk3(U,V,W)),V)
| ~ member(U,comp(V,W)) ),
file('theBenchmark.p',clause81) ).
cnf(clause82,axiom,
( member(idE_sk1(U,V),V)
| ~ member(U,id(V)) ),
file('theBenchmark.p',clause82) ).
cnf(clause83,axiom,
( U = pair(idE_sk1(U,V),idE_sk1(U,V))
| ~ member(U,id(V)) ),
file('theBenchmark.p',clause83) ).
cnf(clause84,axiom,
inr(U) != inl(V),
file('theBenchmark.p',clause84) ).
cnf(clause85,axiom,
inl(U) != inr(V),
file('theBenchmark.p',clause85) ).
cnf(clause86,axiom,
( U = V
| inr(U) != inr(V) ),
file('theBenchmark.p',clause86) ).
cnf(clause87,axiom,
( U = V
| inl(U) != inl(V) ),
file('theBenchmark.p',clause87) ).
cnf(clause88,axiom,
( member(sumE_sk2(U,V,W),W)
| member(sumE_sk1(U,V,W),V)
| ~ member(U,disjsum(V,W)) ),
file('theBenchmark.p',clause88) ).
cnf(clause89,axiom,
( U = inr(sumE_sk2(U,V,W))
| member(sumE_sk1(U,V,W),V)
| ~ member(U,disjsum(V,W)) ),
file('theBenchmark.p',clause89) ).
cnf(clause90,axiom,
( member(sumE_sk2(U,V,W),W)
| U = inl(sumE_sk1(U,V,W))
| ~ member(U,disjsum(V,W)) ),
file('theBenchmark.p',clause90) ).
cnf(clause91,axiom,
( U = inr(sumE_sk2(U,V,W))
| U = inl(sumE_sk1(U,V,W))
| ~ member(U,disjsum(V,W)) ),
file('theBenchmark.p',clause91) ).
cnf(clause92,axiom,
( member(pair(U,vimageE_sk1(U,V,W)),V)
| ~ member(U,vimage(V,W)) ),
file('theBenchmark.p',clause92) ).
cnf(clause93,axiom,
( member(vimageE_sk1(U,V,W),W)
| ~ member(U,vimage(V,W)) ),
file('theBenchmark.p',clause93) ).
cnf(clause94,axiom,
( member(pair(imageE_sk1(U,V,W),U),V)
| ~ member(U,image(V,W)) ),
file('theBenchmark.p',clause94) ).
cnf(clause95,axiom,
( member(imageE_sk1(U,V,W),W)
| ~ member(U,image(V,W)) ),
file('theBenchmark.p',clause95) ).
cnf(clause96,axiom,
( member(pair(fieldE_sk2(U,V),U),V)
| member(pair(U,fieldE_sk1(U,V)),V)
| ~ member(U,field(V)) ),
file('theBenchmark.p',clause96) ).
cnf(clause97,axiom,
( member(pair(rangeE_sk1(U,V),U),V)
| ~ member(U,range(V)) ),
file('theBenchmark.p',clause97) ).
cnf(clause98,axiom,
( member(pair(U,domainE_sk1(U,V)),V)
| ~ member(U,domain(V)) ),
file('theBenchmark.p',clause98) ).
cnf(clause99,axiom,
( member(U,W)
| member(cons_subsetE_sk1(U,V,W),cons(U,V)) ),
file('theBenchmark.p',clause99) ).
cnf(clause100,axiom,
( member(U,W)
| ~ member(cons_subsetE_sk1(U,V,W),W) ),
file('theBenchmark.p',clause100) ).
cnf(clause101,axiom,
( member(U,X)
| member(cons_subsetE_sk1(W,V,X),cons(W,V))
| ~ member(U,V) ),
file('theBenchmark.p',clause101) ).
cnf(clause102,axiom,
( member(X,W)
| ~ member(X,V)
| ~ member(cons_subsetE_sk1(U,V,W),W) ),
file('theBenchmark.p',clause102) ).
cnf(clause102_1,axiom,
( member(A,C)
| ~ subset(cons(A,B),C) ),
file('theBenchmark.p',clause102_1) ).
cnf(clause102_2,axiom,
( subset(B,C)
| ~ subset(cons(A,B),C) ),
file('theBenchmark.p',clause102_2) ).
cnf(clause103,axiom,
( U = pair(converseE_sk2(U,V),converseE_sk1(U,V))
| ~ member(U,converse(V)) ),
file('theBenchmark.p',clause103) ).
cnf(clause104,axiom,
( member(pair(converseE_sk1(U,V),converseE_sk2(U,V)),V)
| ~ member(U,converse(V)) ),
file('theBenchmark.p',clause104) ).
cnf(clause105,axiom,
( member(pair(V,U),W)
| ~ member(pair(U,V),converse(W)) ),
file('theBenchmark.p',clause105) ).
cnf(clause106,axiom,
( U = W
| pair(U,V) != pair(W,X) ),
file('theBenchmark.p',clause106) ).
cnf(clause107,axiom,
( V = X
| pair(U,V) != pair(W,X) ),
file('theBenchmark.p',clause107) ).
cnf(clause108,axiom,
( U = V
| cons(U,eptset) != cons(V,eptset) ),
file('theBenchmark.p',clause108) ).
cnf(clause109,axiom,
( U = V
| succ(U) != succ(V) ),
file('theBenchmark.p',clause109) ).
cnf(clause110,axiom,
( member(U,V)
| U = V
| ~ member(U,succ(V)) ),
file('theBenchmark.p',clause110) ).
cnf(clause111,axiom,
( U = V
| ~ member(U,cons(V,eptset)) ),
file('theBenchmark.p',clause111) ).
cnf(clause112,axiom,
( member(U,W)
| U = V
| ~ member(U,cons(V,W)) ),
file('theBenchmark.p',clause112) ).
cnf(clause113,axiom,
( member(U,V)
| ~ member(U,diff(V,W)) ),
file('theBenchmark.p',clause113) ).
cnf(clause114,axiom,
( ~ member(U,W)
| ~ member(U,diff(V,W)) ),
file('theBenchmark.p',clause114) ).
cnf(clause115,axiom,
( member(U,V)
| ~ member(U,int(V,W)) ),
file('theBenchmark.p',clause115) ).
cnf(clause116,axiom,
( member(U,W)
| ~ member(U,int(V,W)) ),
file('theBenchmark.p',clause116) ).
cnf(clause117,axiom,
( member(U,W)
| member(U,V)
| ~ member(U,un(V,W)) ),
file('theBenchmark.p',clause117) ).
cnf(clause118,axiom,
( member(W,V)
| ~ member(W,U)
| ~ member(U,pow(V)) ),
file('theBenchmark.p',clause118) ).
cnf(clause119,axiom,
( member(U,unionE_sk1(U,V))
| ~ member(U,union(V)) ),
file('theBenchmark.p',clause119) ).
cnf(clause120,axiom,
( member(unionE_sk1(U,V),V)
| ~ member(U,union(V)) ),
file('theBenchmark.p',clause120) ).
cnf(clause121,axiom,
( ~ member(V,U)
| U != eptset ),
file('theBenchmark.p',clause121) ).
cnf(clause122,axiom,
( member(U,W)
| ~ member(W,V)
| ~ member(U,inter(V)) ),
file('theBenchmark.p',clause122) ).
cnf(clause123,axiom,
( member(U,W)
| member(subsetD_sk1(V,W,U),V)
| ~ member(U,V) ),
file('theBenchmark.p',clause123) ).
cnf(clause124,axiom,
( member(W,V)
| ~ member(W,U)
| ~ member(subsetD_sk1(U,V,W),V) ),
file('theBenchmark.p',clause124) ).
cnf(subsetD,axiom,
( member(C,B)
| ~ member(C,A)
| ~ subset(A,B) ),
file('theBenchmark.p',subsetD) ).
cnf(clause125,axiom,
( member(A,field(R))
| ~ member(pair(C,A),R) ),
file('theBenchmark.p',clause125) ).
cnf(clause126,axiom,
( member(A,field(R))
| ~ member(pair(A,B),R) ),
file('theBenchmark.p',clause126) ).
cnf(clause127,axiom,
pair(A,B) != eptset,
file('theBenchmark.p',clause127) ).
cnf(clause128,axiom,
pair(A,B) != A,
file('theBenchmark.p',clause128) ).
cnf(clause129,axiom,
pair(A,B) != B,
file('theBenchmark.p',clause129) ).
cnf(clause131,axiom,
( subset(A,B)
| member(subsetI_sk1(A,B),A) ),
file('theBenchmark.p',clause131) ).
cnf(clause132,axiom,
( subset(A,B)
| ~ member(subsetI_sk1(A,B),B) ),
file('theBenchmark.p',clause132) ).
cnf(clause133,axiom,
subset(A,A),
file('theBenchmark.p',clause133) ).
cnf(clause134,axiom,
( subset(A,C)
| ~ subset(B,C)
| ~ subset(A,B) ),
file('theBenchmark.p',clause134) ).
cnf(clause135,axiom,
( member(X,A)
| ~ member(X,eptset) ),
file('theBenchmark.p',clause135) ).
cnf(clause136,axiom,
subset(eptset,A),
file('theBenchmark.p',clause136) ).
cnf(clause148,axiom,
( A = B
| ~ subset(B,A)
| ~ subset(A,B) ),
file('theBenchmark.p',clause148) ).
cnf(clause149,axiom,
( subset(A,B)
| A != B ),
file('theBenchmark.p',clause149) ).
cnf(clause150,axiom,
( subset(B,A)
| A != B ),
file('theBenchmark.p',clause150) ).
cnf(k_s,axiom,
combK != combS,
file('theBenchmark.p',k_s) ).
cnf(k_app,axiom,
combK != comb_app(P,Q),
file('theBenchmark.p',k_app) ).
cnf(s_app,axiom,
combS != comb_app(P,Q),
file('theBenchmark.p',s_app) ).
cnf(app_app1,axiom,
( P1 = P2
| comb_app(P1,Q1) != comb_app(P2,Q2) ),
file('theBenchmark.p',app_app1) ).
cnf(app_app2,axiom,
( Q1 = Q2
| comb_app(P1,Q1) != comb_app(P2,Q2) ),
file('theBenchmark.p',app_app2) ).
cnf(app_app3,axiom,
( comb_app(P1,Q1) = comb_app(P2,Q2)
| Q1 != Q2
| P1 != P2 ),
file('theBenchmark.p',app_app3) ).
cnf(r_into_trancl,axiom,
( member(pair(A,B),trancl(R))
| ~ member(pair(A,B),R) ),
file('theBenchmark.p',r_into_trancl) ).
cnf(trans_trancl,axiom,
trans(trancl(R)),
file('theBenchmark.p',trans_trancl) ).
cnf(transD,axiom,
( member(pair(A,C),R)
| ~ member(pair(B,C),R)
| ~ member(pair(A,B),R)
| ~ trans(R) ),
file('theBenchmark.p',transD) ).
cnf(diamond_strip_lemmaD1,axiom,
( member(pair(YP,diamond_strip_lemmaD_sk1(X,Y,YP,R)),trancl(R))
| ~ member(pair(X,YP),R)
| ~ member(pair(X,Y),trancl(R))
| ~ diamond(R) ),
file('theBenchmark.p',diamond_strip_lemmaD1) ).
cnf(diamond_strip_lemmaD2,axiom,
( member(pair(Y,diamond_strip_lemmaD_sk1(X,Y,YP,R)),R)
| ~ member(pair(X,YP),R)
| ~ member(pair(X,Y),trancl(R))
| ~ diamond(R) ),
file('theBenchmark.p',diamond_strip_lemmaD2) ).
cnf(diamond_trancl_1h1,hypothesis,
diamond(r),
file('theBenchmark.p',diamond_trancl_1h1) ).
cnf(diamond_trancl_1h2,hypothesis,
member(pair(y,ya),r),
file('theBenchmark.p',diamond_trancl_1h2) ).
cnf(diamond_trancl_1c1,negated_conjecture,
member(pair(y,yp),trancl(r)),
file('theBenchmark.p',diamond_trancl_1c1) ).
cnf(diamond_trancl_1c2,negated_conjecture,
( ~ member(pair(yp,Z),trancl(r))
| ~ member(pair(ya,Z),trancl(r)) ),
file('theBenchmark.p',diamond_trancl_1c2) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( cons(Eq_x_0,Eq_x_1) = cons(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( succ(Eq_x_0) = succ(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( inr(Eq_x_0) = inr(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( inl(Eq_x_0) = inl(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( disjsum(Eq_x_0,Eq_x_1) = disjsum(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( cons_subsetI_sk1(Eq_x_0,Eq_x_1,Eq_x_2) = cons_subsetI_sk1(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,axiom,
( pair(Eq_x_0,Eq_x_1) = pair(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_11,axiom,
( converse(Eq_x_0) = converse(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_12,axiom,
( diff(Eq_x_0,Eq_x_1) = diff(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_13,axiom,
( int(Eq_x_0,Eq_x_1) = int(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_14,axiom,
( un(Eq_x_0,Eq_x_1) = un(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_15,axiom,
( powI_sk1(Eq_x_0,Eq_x_1) = powI_sk1(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_16,axiom,
( pow(Eq_x_0) = pow(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_17,axiom,
( interI_sk1(Eq_x_0,Eq_x_1) = interI_sk1(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_18,axiom,
( inter(Eq_x_0) = inter(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_19,axiom,
( card_Union_sk1(Eq_x_0) = card_Union_sk1(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_20,axiom,
( union(Eq_x_0) = union(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_21,axiom,
( fin(Eq_x_0) = fin(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_22,axiom,
( order_Inter_sk1(Eq_x_0) = order_Inter_sk1(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_23,axiom,
( order_Union_sk1(Eq_x_0) = order_Union_sk1(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_24,axiom,
( comp(Eq_x_0,Eq_x_1) = comp(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_25,axiom,
( vimage(Eq_x_0,Eq_x_1) = vimage(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_26,axiom,
( image(Eq_x_0,Eq_x_1) = image(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_27,axiom,
( qInr(Eq_x_0) = qInr(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_28,axiom,
( qInl(Eq_x_0) = qInl(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_29,axiom,
( qsum(Eq_x_0,Eq_x_1) = qsum(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_30,axiom,
( qsumE_sk1(Eq_x_0,Eq_x_1,Eq_x_2) = qsumE_sk1(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_31,axiom,
( qsumE_sk2(Eq_x_0,Eq_x_1,Eq_x_2) = qsumE_sk2(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_32,axiom,
( qconverse(Eq_x_0) = qconverse(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_33,axiom,
( qconverseE_sk2(Eq_x_0,Eq_x_1) = qconverseE_sk2(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_34,axiom,
( qconverseE_sk1(Eq_x_0,Eq_x_1) = qconverseE_sk1(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_35,axiom,
( qPair(Eq_x_0,Eq_x_1) = qPair(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_36,axiom,
( rmult(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = rmult(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_37,axiom,
( radd(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = radd(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_38,axiom,
( memrel(Eq_x_0) = memrel(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_39,axiom,
( compE_sk1(Eq_x_0,Eq_x_1,Eq_x_2) = compE_sk1(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_40,axiom,
( compE_sk3(Eq_x_0,Eq_x_1,Eq_x_2) = compE_sk3(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_41,axiom,
( compE_sk2(Eq_x_0,Eq_x_1,Eq_x_2) = compE_sk2(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_42,axiom,
( id(Eq_x_0) = id(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_43,axiom,
( idE_sk1(Eq_x_0,Eq_x_1) = idE_sk1(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_44,axiom,
( sumE_sk1(Eq_x_0,Eq_x_1,Eq_x_2) = sumE_sk1(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_45,axiom,
( sumE_sk2(Eq_x_0,Eq_x_1,Eq_x_2) = sumE_sk2(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_46,axiom,
( vimageE_sk1(Eq_x_0,Eq_x_1,Eq_x_2) = vimageE_sk1(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_47,axiom,
( imageE_sk1(Eq_x_0,Eq_x_1,Eq_x_2) = imageE_sk1(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_48,axiom,
( field(Eq_x_0) = field(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_49,axiom,
( fieldE_sk1(Eq_x_0,Eq_x_1) = fieldE_sk1(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_50,axiom,
( fieldE_sk2(Eq_x_0,Eq_x_1) = fieldE_sk2(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_51,axiom,
( range(Eq_x_0) = range(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_52,axiom,
( rangeE_sk1(Eq_x_0,Eq_x_1) = rangeE_sk1(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_53,axiom,
( domain(Eq_x_0) = domain(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_54,axiom,
( domainE_sk1(Eq_x_0,Eq_x_1) = domainE_sk1(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_55,axiom,
( cons_subsetE_sk1(Eq_x_0,Eq_x_1,Eq_x_2) = cons_subsetE_sk1(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_56,axiom,
( converseE_sk2(Eq_x_0,Eq_x_1) = converseE_sk2(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_57,axiom,
( converseE_sk1(Eq_x_0,Eq_x_1) = converseE_sk1(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_58,axiom,
( unionE_sk1(Eq_x_0,Eq_x_1) = unionE_sk1(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_59,axiom,
( subsetD_sk1(Eq_x_0,Eq_x_1,Eq_x_2) = subsetD_sk1(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_60,axiom,
( subsetI_sk1(Eq_x_0,Eq_x_1) = subsetI_sk1(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_61,axiom,
( comb_app(Eq_x_0,Eq_x_1) = comb_app(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_62,axiom,
( trancl(Eq_x_0) = trancl(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_63,axiom,
( diamond_strip_lemmaD_sk1(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = diamond_strip_lemmaD_sk1(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_64,axiom,
( member(Eq_y_0,Eq_y_1)
| ~ member(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_65,axiom,
( subset(Eq_y_0,Eq_y_1)
| ~ subset(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_66,axiom,
( card(Eq_y_0)
| ~ card(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_67,axiom,
( ord(Eq_y_0)
| ~ ord(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_68,axiom,
( rmultE_c1(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4,Eq_y_5,Eq_y_6,Eq_y_7)
| ~ rmultE_c1(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4,Eq_x_5,Eq_x_6,Eq_x_7)
| Eq_x_7 != Eq_y_7
| Eq_x_6 != Eq_y_6
| Eq_x_5 != Eq_y_5
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_69,axiom,
( rmultE_c2(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4,Eq_y_5,Eq_y_6,Eq_y_7)
| ~ rmultE_c2(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4,Eq_x_5,Eq_x_6,Eq_x_7)
| Eq_x_7 != Eq_y_7
| Eq_x_6 != Eq_y_6
| Eq_x_5 != Eq_y_5
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_70,axiom,
( le(Eq_y_0,Eq_y_1)
| ~ le(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_71,axiom,
( lt(Eq_y_0,Eq_y_1)
| ~ lt(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_72,axiom,
( trans(Eq_y_0)
| ~ trans(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_73,axiom,
( diamond(Eq_y_0)
| ~ diamond(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COL099-2 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.03 This is a CNF_UNS_RFO_SEQ_NHN problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n008.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 20 14:57:11 UTC 2026
% 0.09/0.37 % CPUTime :
% 12.16/12.42 % SZS status Unsatisfiable for theBenchmark
% 12.16/12.42 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------