↑ Up

Fiesta---2.UNS-CRf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Fiesta---2
% Problem  : LAT012-1 : TPTP v8.1.0. Released v2.2.0.
% Transfm  : none
% Format   : dedam
% Command  : fiesta-wrapper %s

% Computer : n004.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 04:55:24 EDT 2022

% Result   : Unsatisfiable 1.95s 2.33s
% Output   : CNFRefutation 1.95s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11  % Problem  : LAT012-1 : TPTP v8.1.0. Released v2.2.0.
% 0.03/0.12  % Command  : fiesta-wrapper %s
% 0.11/0.33  % Computer : n004.cluster.edu
% 0.11/0.33  % Model    : x86_64 x86_64
% 0.11/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33  % Memory   : 8042.1875MB
% 0.11/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33  % CPULimit : 300
% 0.11/0.33  % WCLimit  : 600
% 0.11/0.33  % DateTime : Wed Jun 29 13:28:08 EDT 2022
% 0.11/0.33  % CPUTime  : 
% 1.95/2.33  Theorem Proved.
% 1.95/2.33  % SZS status Unsatisfiable
% 1.95/2.33  % SZS output start CNFRefutation
% 1.95/2.33  [1=axiom,[],
% 1.95/2.33  			meet(meet(join(X10,X11),join(X11,X12)),X11) 	= X11].
% 1.95/2.33  [2=axiom,[],
% 1.95/2.33  			join(join(meet(X10,X11),meet(X11,X12)),X11) 	= X11].
% 1.95/2.33  [3=axiom,[],
% 1.95/2.33  			meet(X10,join(X11,join(X10,X12))) 	= X10].
% 1.95/2.33  [4=axiom,[],
% 1.95/2.33  			join(X10,meet(X11,meet(X10,X12))) 	= X10].
% 1.95/2.33  [5=axiom,[],
% 1.95/2.33  			thtop(X10,X10) 	= thmfalse].
% 1.95/2.33  [6=axiom,[],
% 1.95/2.33  			thtop(meet(b,a),meet(a,b)) 	= thmtrue].
% 1.95/2.33  [7=param(4,1),[],
% 1.95/2.33  			join(X10,meet(X10,X11)) 	= X10].
% 1.95/2.33  [8=param(1,4),[],
% 1.95/2.33  			meet(meet(join(X10,X11),X11),X11) 	= X11].
% 1.95/2.33  [9=param(1,7),[],
% 1.95/2.33  			meet(meet(X10,join(meet(X10,X11),X12)),meet(X10,X11)) 	= meet(X10,X11)].
% 1.95/2.33  [12=param(2,4),[],
% 1.95/2.33  			join(meet(X10,X11),X11) 	= X11].
% 1.95/2.33  [13=param(1,12),[],
% 1.95/2.33  			meet(meet(join(X10,meet(X11,X12)),X12),meet(X11,X12)) 	= meet(X11,X12)].
% 1.95/2.33  [14=param(1,3),[],
% 1.95/2.33  			meet(join(X10,X11),X11) 	= X11].
% 1.95/2.33  [15=demod(8),[14],
% 1.95/2.33  			meet(X10,X10) 	= X10].
% 1.95/2.33  [16=param(3,2),[],
% 1.95/2.33  			meet(X10,join(X10,X11)) 	= X10].
% 1.95/2.33  [17=param(3,4),[],
% 1.95/2.33  			meet(X10,join(X11,X10)) 	= X10].
% 1.95/2.33  [18=param(4,3),[],
% 1.95/2.33  			join(X10,meet(X11,X10)) 	= X10].
% 1.95/2.33  [19=param(3,12),[],
% 1.95/2.33  			meet(meet(X10,X11),join(X12,X11)) 	= meet(X10,X11)].
% 1.95/2.33  [20=param(1,18),[],
% 1.95/2.33  			meet(meet(X10,join(meet(X11,X10),X12)),meet(X11,X10)) 	= meet(X11,X10)].
% 1.95/2.33  [23=param(2,17),[],
% 1.95/2.33  			join(join(X10,meet(join(X11,X10),X12)),join(X11,X10)) 	= join(X11,X10)].
% 1.95/2.33  [24=param(17,4),[],
% 1.95/2.33  			meet(meet(X10,meet(X11,X12)),X11) 	= meet(X10,meet(X11,X12))].
% 1.95/2.33  [25=param(17,7),[],
% 1.95/2.33  			meet(meet(X10,X11),X10) 	= meet(X10,X11)].
% 1.95/2.33  [27=param(18,17),[],
% 1.95/2.33  			join(join(X10,X11),X11) 	= join(X10,X11)].
% 1.95/2.33  [28=param(2,16),[],
% 1.95/2.33  			join(join(X10,meet(join(X10,X11),X12)),join(X10,X11)) 	= join(X10,X11)].
% 1.95/2.33  [31=param(13,18),[15],
% 1.95/2.33  			meet(X10,meet(X11,X10)) 	= meet(X11,X10)].
% 1.95/2.33  [34=param(4,14),[],
% 1.95/2.33  			join(join(X10,X11),meet(X12,X11)) 	= join(X10,X11)].
% 1.95/2.33  [36=param(31,3),[3],
% 1.95/2.33  			meet(join(X10,join(X11,X12)),X11) 	= X11].
% 1.95/2.33  [37=param(4,31),[],
% 1.95/2.33  			join(X10,meet(X11,meet(X12,X10))) 	= X10].
% 1.95/2.33  [38=param(31,16),[16],
% 1.95/2.33  			meet(join(X10,X11),X10) 	= X10].
% 1.95/2.33  [39=param(19,18),[],
% 1.95/2.33  			meet(meet(X10,meet(X11,X12)),X12) 	= meet(X10,meet(X11,X12))].
% 1.95/2.33  [42=param(4,38),[],
% 1.95/2.33  			join(join(X10,X11),meet(X12,X10)) 	= join(X10,X11)].
% 1.95/2.33  [51=param(4,25),[],
% 1.95/2.33  			join(X10,meet(meet(X10,X11),X12)) 	= X10].
% 1.95/2.33  [52=param(23,3),[27],
% 1.95/2.33  			join(X10,join(X11,X10)) 	= join(X11,X10)].
% 1.95/2.33  [54=param(23,38),[],
% 1.95/2.33  			join(join(X10,X11),join(X11,X10)) 	= join(X11,X10)].
% 1.95/2.33  [56=param(3,52),[],
% 1.95/2.33  			meet(X10,join(X11,join(X12,X10))) 	= X10].
% 1.95/2.33  [62=param(31,56),[56],
% 1.95/2.33  			meet(join(X10,join(X11,X12)),X12) 	= X12].
% 1.95/2.33  [70=param(28,62),[],
% 1.95/2.33  			join(join(X10,X11),join(X10,join(X12,X11))) 	= join(X10,join(X12,X11))].
% 1.95/2.33  [75=param(13,51),[],
% 1.95/2.33  			meet(meet(X10,X11),meet(meet(X10,X12),X11)) 	= meet(meet(X10,X12),X11)].
% 1.95/2.33  [89=param(37,25),[],
% 1.95/2.33  			join(X10,meet(meet(X11,X10),X12)) 	= X10].
% 1.95/2.33  [92=param(34,25),[],
% 1.95/2.33  			join(join(X10,X11),meet(X11,X12)) 	= join(X10,X11)].
% 1.95/2.33  [93=param(13,89),[],
% 1.95/2.33  			meet(meet(X10,X11),meet(meet(X12,X10),X11)) 	= meet(meet(X12,X10),X11)].
% 1.95/2.33  [96=param(28,36),[],
% 1.95/2.33  			join(join(X10,X11),join(X10,join(X11,X12))) 	= join(X10,join(X11,X12))].
% 1.95/2.33  [110=param(3,54),[],
% 1.95/2.33  			meet(join(X10,X11),join(X12,join(X11,X10))) 	= join(X10,X11)].
% 1.95/2.33  [111=param(16,54),[],
% 1.95/2.33  			meet(join(X10,X11),join(X11,X10)) 	= join(X10,X11)].
% 1.95/2.33  [113=param(18,111),[54],
% 1.95/2.33  			join(X10,X11) 	= join(X11,X10)].
% 1.95/2.33  [125=demod(23),[113],
% 1.95/2.33  			join(join(X10,X11),join(X11,meet(join(X10,X11),X12))) 	= join(X10,X11)].
% 1.95/2.33  [136=param(113,34),[],
% 1.95/2.33  			join(meet(X10,X11),join(X12,X11)) 	= join(X12,X11)].
% 1.95/2.33  [137=param(113,92),[],
% 1.95/2.33  			join(meet(X10,X11),join(X12,X10)) 	= join(X12,X10)].
% 1.95/2.33  [141=param(42,25),[],
% 1.95/2.33  			join(join(X10,X11),meet(X10,X12)) 	= join(X10,X11)].
% 1.95/2.33  [148=param(14,141),[],
% 1.95/2.33  			meet(join(X10,X11),meet(X10,X12)) 	= meet(X10,X12)].
% 1.95/2.33  [158=param(20,137),[],
% 1.95/2.33  			meet(meet(X10,join(X11,X12)),meet(X12,X10)) 	= meet(X12,X10)].
% 1.95/2.33  [160=param(9,136),[],
% 1.95/2.33  			meet(meet(X10,join(X11,X12)),meet(X10,X12)) 	= meet(X10,X12)].
% 1.95/2.33  [200=param(70,113),[],
% 1.95/2.33  			join(join(X10,X11),join(X11,join(X12,X10))) 	= join(X11,join(X12,X10))].
% 1.95/2.33  [217=param(4,75),[],
% 1.95/2.33  			join(meet(X10,X11),meet(X12,meet(meet(X10,X13),X11))) 	= meet(X10,X11)].
% 1.95/2.33  [256=param(4,93),[],
% 1.95/2.33  			join(meet(X10,X11),meet(X12,meet(meet(X13,X10),X11))) 	= meet(X10,X11)].
% 1.95/2.33  [261=param(16,96),[],
% 1.95/2.33  			meet(join(X10,X11),join(X10,join(X11,X12))) 	= join(X10,X11)].
% 1.95/2.33  [262=param(96,113),[],
% 1.95/2.33  			join(join(X10,X11),join(X11,join(X10,X12))) 	= join(X11,join(X10,X12))].
% 1.95/2.33  [263=param(31,261),[261],
% 1.95/2.33  			meet(join(X10,join(X11,X12)),join(X10,X11)) 	= join(X10,X11)].
% 1.95/2.33  [274=param(110,113),[],
% 1.95/2.33  			meet(join(X10,X11),join(join(X11,X10),X12)) 	= join(X10,X11)].
% 1.95/2.33  [276=param(274,70),[],
% 1.95/2.33  			meet(join(X10,X11),join(X11,join(X12,X10))) 	= join(X10,X11)].
% 1.95/2.33  [290=param(31,276),[276],
% 1.95/2.33  			meet(join(X10,join(X11,X12)),join(X12,X10)) 	= join(X12,X10)].
% 1.95/2.33  [305=param(125,148),[],
% 1.95/2.33  			join(join(X10,X11),join(X11,meet(X10,X12))) 	= join(X10,X11)].
% 1.95/2.33  [306=param(125,263),[262],
% 1.95/2.33  			join(join(X10,X11),join(X12,X10)) 	= join(X12,join(X10,X11))].
% 1.95/2.33  [308=param(125,290),[200],
% 1.95/2.33  			join(join(X10,X11),join(X11,X12)) 	= join(X12,join(X10,X11))].
% 1.95/2.33  [313=param(305,113),[306],
% 1.95/2.33  			join(X10,join(X11,meet(X10,X12))) 	= join(X10,X11)].
% 1.95/2.33  [320=param(313,38),[],
% 1.95/2.33  			join(join(X10,X11),join(X12,X10)) 	= join(join(X10,X11),X12)].
% 1.95/2.33  [361=param(320,113),[],
% 1.95/2.33  			join(join(X10,X11),join(X10,X12)) 	= join(join(X10,X11),X12)].
% 1.95/2.33  [363=demod(96),[361],
% 1.95/2.33  			join(join(X10,X11),join(X11,X12)) 	= join(X10,join(X11,X12))].
% 1.95/2.33  [364=demod(308),[363],
% 1.95/2.33  			join(X10,join(X11,X12)) 	= join(X12,join(X10,X11))].
% 1.95/2.33  [492=param(217,1),[],
% 1.95/2.33  			join(meet(X10,X11),meet(meet(X10,X12),X11)) 	= meet(X10,X11)].
% 1.95/2.33  [494=param(17,492),[],
% 1.95/2.33  			meet(meet(meet(X10,X11),X12),meet(X10,X12)) 	= meet(meet(X10,X11),X12)].
% 1.95/2.33  [524=param(256,1),[],
% 1.95/2.33  			join(meet(X10,X11),meet(meet(X12,X10),X11)) 	= meet(X10,X11)].
% 1.95/2.33  [527=param(17,524),[],
% 1.95/2.33  			meet(meet(meet(X10,X11),X12),meet(X11,X12)) 	= meet(meet(X10,X11),X12)].
% 1.95/2.33  [637=param(313,75),[],
% 1.95/2.33  			join(meet(X10,X11),join(X12,meet(meet(X10,X13),X11))) 	= join(meet(X10,X11),X12)].
% 1.95/2.33  [734=param(4,158),[],
% 1.95/2.33  			join(meet(X10,join(X11,X12)),meet(X13,meet(X12,X10))) 	= meet(X10,join(X11,X12))].
% 1.95/2.33  [736=param(4,160),[],
% 1.95/2.33  			join(meet(X10,join(X11,X12)),meet(X13,meet(X10,X12))) 	= meet(X10,join(X11,X12))].
% 1.95/2.33  [1234=param(736,1),[113],
% 1.95/2.33  			join(meet(X10,X11),meet(X10,join(X12,X11))) 	= meet(X10,join(X12,X11))].
% 1.95/2.33  [1243=param(20,1234),[],
% 1.95/2.33  			meet(meet(X10,meet(X11,join(X12,X10))),meet(X11,X10)) 	= meet(X11,X10)].
% 1.95/2.33  [1301=param(734,1),[],
% 1.95/2.33  			join(meet(X10,join(X11,X12)),meet(X12,X10)) 	= meet(X10,join(X11,X12))].
% 1.95/2.33  [1309=param(1301,113),[],
% 1.95/2.33  			join(meet(X12,X10),meet(X10,join(X11,X12))) 	= meet(X10,join(X11,X12))].
% 1.95/2.33  [1314=param(9,1309),[],
% 1.95/2.33  			meet(meet(X10,meet(X11,join(X12,X10))),meet(X10,X11)) 	= meet(X10,X11)].
% 1.95/2.33  [1399=param(637,364),[],
% 1.95/2.33  			join(meet(meet(X10,X13),X11),join(meet(X10,X11),X12)) 	= join(meet(X10,X11),X12)].
% 1.95/2.33  [1402=param(1399,39),[],
% 1.95/2.33  			join(meet(X10,meet(X11,X12)),join(meet(X10,X12),X13)) 	= join(meet(X10,X12),X13)].
% 1.95/2.33  [1403=param(1402,4),[113,4],
% 1.95/2.33  			join(meet(X10,X11),meet(X10,meet(X12,X11))) 	= meet(X10,X11)].
% 1.95/2.33  [1416=param(13,1403),[494],
% 1.95/2.33  			meet(meet(X10,X11),meet(X12,X11)) 	= meet(X10,meet(X12,X11))].
% 1.95/2.33  [1417=demod(494),[1416],
% 1.95/2.33  			meet(meet(X10,X11),meet(X10,X12)) 	= meet(meet(X10,X11),X12)].
% 1.95/2.33  [1427=demod(1314),[1417,24],
% 1.95/2.33  			meet(X10,meet(X11,join(X12,X10))) 	= meet(X10,X11)].
% 1.95/2.33  [1428=demod(1243),[1427],
% 1.95/2.33  			meet(meet(X10,X11),meet(X11,X10)) 	= meet(X11,X10)].
% 1.95/2.33  [1430=demod(527),[1416],
% 1.95/2.33  			meet(meet(X10,X11),meet(X11,X12)) 	= meet(meet(X10,X11),X12)].
% 1.95/2.33  [1431=demod(1428),[1430,25],
% 1.95/2.33  			meet(X10,X11) 	= meet(X11,X10)].
% 1.95/2.33  [1449=param(6,1431),[5],
% 1.95/2.33  			thmtrue 	= thmfalse].
% 1.95/2.33  % SZS output end CNFRefutation
% 1.95/2.33  Space:   5757 KB 
%------------------------------------------------------------------------------