↑ Up

Fiesta---2.UNS-CRf.s

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

% Computer : n023.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 0.83s 1.21s
% Output   : CNFRefutation 0.83s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11  % Problem  : LAT013-1 : TPTP v8.1.0. Released v2.2.0.
% 0.06/0.12  % Command  : fiesta-wrapper %s
% 0.12/0.31  % Computer : n023.cluster.edu
% 0.12/0.31  % Model    : x86_64 x86_64
% 0.12/0.31  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.31  % Memory   : 8042.1875MB
% 0.12/0.31  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.31  % CPULimit : 300
% 0.12/0.31  % WCLimit  : 600
% 0.12/0.31  % DateTime : Wed Jun 29 01:56:30 EDT 2022
% 0.16/0.31  % CPUTime  : 
% 0.83/1.21  Theorem Proved.
% 0.83/1.21  % SZS status Unsatisfiable
% 0.83/1.21  % SZS output start CNFRefutation
% 0.83/1.21  [1=axiom,[],
% 0.83/1.21  			meet(meet(join(X10,X11),join(X11,X12)),X11) 	= X11].
% 0.83/1.21  [2=axiom,[],
% 0.83/1.21  			join(join(meet(X10,X11),meet(X11,X12)),X11) 	= X11].
% 0.83/1.21  [3=axiom,[],
% 0.83/1.21  			meet(X10,join(X11,join(X10,X12))) 	= X10].
% 0.83/1.21  [4=axiom,[],
% 0.83/1.21  			join(X10,meet(X11,meet(X10,X12))) 	= X10].
% 0.83/1.21  [5=axiom,[],
% 0.83/1.21  			thtop(X10,X10) 	= thmfalse].
% 0.83/1.21  [6=axiom,[],
% 0.83/1.21  			thtop(meet(meet(a,b),c),meet(a,meet(b,c))) 	= thmtrue].
% 0.83/1.21  [7=param(3,4),[],
% 0.83/1.21  			meet(X10,join(X11,X10)) 	= X10].
% 0.83/1.21  [8=param(4,3),[],
% 0.83/1.21  			join(X10,meet(X11,X10)) 	= X10].
% 0.83/1.21  [9=param(8,3),[],
% 0.83/1.21  			join(join(X10,join(X11,X12)),X11) 	= join(X10,join(X11,X12))].
% 0.83/1.21  [10=param(1,3),[],
% 0.83/1.21  			meet(join(X10,X11),X11) 	= X11].
% 0.83/1.21  [11=param(1,4),[10],
% 0.83/1.21  			meet(X10,X10) 	= X10].
% 0.83/1.21  [12=param(4,1),[],
% 0.83/1.21  			join(X10,meet(X10,X11)) 	= X10].
% 0.83/1.21  [13=param(1,8),[],
% 0.83/1.21  			meet(meet(X10,join(meet(X11,X10),X12)),meet(X11,X10)) 	= meet(X11,X10)].
% 0.83/1.21  [14=param(8,1),[],
% 0.83/1.21  			join(X10,X10) 	= X10].
% 0.83/1.21  [16=param(3,14),[],
% 0.83/1.21  			meet(X10,join(X10,X11)) 	= X10].
% 0.83/1.21  [18=param(2,4),[],
% 0.83/1.21  			join(meet(X10,X11),X11) 	= X11].
% 0.83/1.21  [19=param(1,18),[],
% 0.83/1.21  			meet(meet(join(X10,meet(X11,X12)),X12),meet(X11,X12)) 	= meet(X11,X12)].
% 0.83/1.21  [22=param(2,16),[],
% 0.83/1.21  			join(join(X10,meet(join(X10,X11),X12)),join(X10,X11)) 	= join(X10,X11)].
% 0.83/1.21  [23=param(8,16),[],
% 0.83/1.21  			join(join(X10,X11),X10) 	= join(X10,X11)].
% 0.83/1.21  [26=param(2,7),[],
% 0.83/1.21  			join(join(X10,meet(join(X11,X10),X12)),join(X11,X10)) 	= join(X11,X10)].
% 0.83/1.21  [27=param(7,4),[],
% 0.83/1.21  			meet(meet(X10,meet(X11,X12)),X11) 	= meet(X10,meet(X11,X12))].
% 0.83/1.21  [29=param(18,7),[],
% 0.83/1.21  			join(X10,join(X11,X10)) 	= join(X11,X10)].
% 0.83/1.21  [30=param(1,12),[],
% 0.83/1.21  			meet(meet(X10,join(meet(X10,X11),X12)),meet(X10,X11)) 	= meet(X10,X11)].
% 0.83/1.21  [31=param(7,12),[],
% 0.83/1.21  			meet(meet(X10,X11),X10) 	= meet(X10,X11)].
% 0.83/1.21  [32=param(2,10),[],
% 0.83/1.21  			join(join(meet(X10,join(X11,X12)),X12),join(X11,X12)) 	= join(X11,X12)].
% 0.83/1.21  [33=param(4,10),[],
% 0.83/1.21  			join(join(X10,X11),meet(X12,X11)) 	= join(X10,X11)].
% 0.83/1.21  [34=param(1,9),[],
% 0.83/1.21  			meet(meet(join(X10,join(X11,X12)),join(X11,X13)),X11) 	= X11].
% 0.83/1.21  [37=param(4,31),[],
% 0.83/1.21  			join(X10,meet(meet(X10,X11),X12)) 	= X10].
% 0.83/1.21  [38=param(18,31),[],
% 0.83/1.21  			join(meet(X10,X11),X10) 	= X10].
% 0.83/1.21  [39=param(1,38),[],
% 0.83/1.21  			meet(meet(join(X10,meet(X11,X12)),X11),meet(X11,X12)) 	= meet(X11,X12)].
% 0.83/1.21  [41=param(13,3),[],
% 0.83/1.21  			meet(X10,meet(X11,X10)) 	= meet(X11,X10)].
% 0.83/1.21  [42=param(13,38),[],
% 0.83/1.21  			meet(meet(X10,X11),meet(X11,X10)) 	= meet(X11,X10)].
% 0.83/1.21  [44=param(4,41),[],
% 0.83/1.21  			join(X10,meet(X11,meet(X12,X10))) 	= X10].
% 0.83/1.21  [46=param(3,29),[],
% 0.83/1.21  			meet(X10,join(X11,join(X12,X10))) 	= X10].
% 0.83/1.21  [62=param(46,23),[],
% 0.83/1.21  			meet(X10,join(join(X11,X10),X12)) 	= X10].
% 0.83/1.21  [66=param(44,31),[],
% 0.83/1.21  			join(X10,meet(meet(X11,X10),X12)) 	= X10].
% 0.83/1.21  [69=param(19,66),[],
% 0.83/1.21  			meet(meet(X10,X11),meet(meet(X12,X10),X11)) 	= meet(meet(X12,X10),X11)].
% 0.83/1.21  [71=param(19,37),[],
% 0.83/1.21  			meet(meet(X10,X11),meet(meet(X10,X12),X11)) 	= meet(meet(X10,X12),X11)].
% 0.83/1.21  [74=param(18,27),[],
% 0.83/1.21  			join(meet(X10,meet(X11,X12)),X11) 	= X11].
% 0.83/1.21  [81=param(30,74),[],
% 0.83/1.21  			meet(meet(X10,X11),meet(X10,meet(X11,X12))) 	= meet(X10,meet(X11,X12))].
% 0.83/1.21  [86=param(32,62),[],
% 0.83/1.21  			join(join(X10,X11),join(join(X12,X10),X11)) 	= join(join(X12,X10),X11)].
% 0.83/1.21  [94=param(33,31),[],
% 0.83/1.21  			join(join(X10,X11),meet(X11,X12)) 	= join(X10,X11)].
% 0.83/1.21  [96=param(19,94),[],
% 0.83/1.21  			meet(meet(join(X10,X11),X12),meet(X11,X12)) 	= meet(X11,X12)].
% 0.83/1.21  [97=param(4,42),[],
% 0.83/1.21  			join(meet(X10,X11),meet(X12,meet(X11,X10))) 	= meet(X10,X11)].
% 0.83/1.21  [98=param(34,3),[],
% 0.83/1.21  			meet(join(X10,join(X11,X12)),X11) 	= X11].
% 0.83/1.21  [99=param(34,10),[],
% 0.83/1.21  			meet(join(X10,X11),X10) 	= X10].
% 0.83/1.21  [103=param(26,99),[],
% 0.83/1.21  			join(join(X10,X11),join(X11,X10)) 	= join(X11,X10)].
% 0.83/1.21  [107=param(22,98),[],
% 0.83/1.21  			join(join(X10,X11),join(X10,join(X11,X12))) 	= join(X10,join(X11,X12))].
% 0.83/1.21  [114=param(3,103),[],
% 0.83/1.21  			meet(join(X10,X11),join(X12,join(X11,X10))) 	= join(X10,X11)].
% 0.83/1.21  [115=param(16,103),[],
% 0.83/1.21  			meet(join(X10,X11),join(X11,X10)) 	= join(X10,X11)].
% 0.83/1.21  [116=param(99,103),[115],
% 0.83/1.21  			join(X10,X11) 	= join(X11,X10)].
% 0.83/1.21  [120=demod(22),[116],
% 0.83/1.21  			join(join(X10,X11),join(X10,meet(join(X10,X11),X12))) 	= join(X10,X11)].
% 0.83/1.21  [129=param(39,4),[],
% 0.83/1.21  			meet(meet(X10,X11),meet(X11,meet(X10,X12))) 	= meet(X11,meet(X10,X12))].
% 0.83/1.21  [207=param(4,69),[],
% 0.83/1.21  			join(meet(X10,X11),meet(X12,meet(meet(X13,X10),X11))) 	= meet(X10,X11)].
% 0.83/1.21  [221=param(4,81),[],
% 0.83/1.21  			join(meet(X10,X11),meet(X12,meet(X10,meet(X11,X13)))) 	= meet(X10,X11)].
% 0.83/1.21  [252=param(114,116),[],
% 0.83/1.21  			meet(join(X10,X11),join(join(X11,X10),X12)) 	= join(X10,X11)].
% 0.83/1.21  [259=param(252,86),[],
% 0.83/1.21  			meet(join(X10,X11),join(join(X12,X11),X10)) 	= join(X10,X11)].
% 0.83/1.21  [261=param(97,1),[],
% 0.83/1.21  			join(meet(X10,X11),meet(X11,X10)) 	= meet(X10,X11)].
% 0.83/1.21  [269=param(7,261),[42],
% 0.83/1.21  			meet(X10,X11) 	= meet(X11,X10)].
% 0.83/1.21  [289=demod(96),[269],
% 0.83/1.21  			meet(meet(X10,X11),meet(join(X12,X10),X11)) 	= meet(X10,X11)].
% 0.83/1.21  [323=param(269,259),[],
% 0.83/1.21  			meet(join(join(X10,X11),X12),join(X12,X11)) 	= join(X12,X11)].
% 0.83/1.21  [328=param(107,116),[],
% 0.83/1.21  			join(join(X10,X11),join(X11,join(X10,X12))) 	= join(X11,join(X10,X12))].
% 0.83/1.21  [367=param(129,269),[],
% 0.83/1.21  			meet(meet(X10,meet(X11,X12)),meet(X11,X10)) 	= meet(X10,meet(X11,X12))].
% 0.83/1.21  [373=param(120,323),[107],
% 0.83/1.21  			join(join(X10,X11),join(X12,X11)) 	= join(join(X10,X11),X12)].
% 0.83/1.21  [378=param(373,12),[12],
% 0.83/1.21  			join(X10,join(X11,meet(X10,X12))) 	= join(X10,X11)].
% 0.83/1.21  [387=param(373,116),[],
% 0.83/1.21  			join(join(X10,X11),join(X11,X12)) 	= join(join(X10,X11),X12)].
% 0.83/1.21  [388=demod(328),[387],
% 0.83/1.21  			join(join(X10,X11),join(X10,X12)) 	= join(X11,join(X10,X12))].
% 0.83/1.21  [392=param(373,261),[261],
% 0.83/1.21  			join(meet(X10,X11),join(X12,meet(X11,X10))) 	= join(meet(X10,X11),X12)].
% 0.83/1.21  [394=param(378,116),[],
% 0.83/1.21  			join(X10,join(meet(X10,X11),X12)) 	= join(X10,X12)].
% 0.83/1.21  [395=param(394,41),[],
% 0.83/1.21  			join(X10,join(meet(X11,X10),X12)) 	= join(X10,X12)].
% 0.83/1.21  [396=param(394,42),[],
% 0.83/1.21  			join(meet(X10,X11),join(meet(X11,X10),X12)) 	= join(meet(X10,X11),X12)].
% 0.83/1.21  [411=param(395,16),[388],
% 0.83/1.21  			join(join(X11,X10),X12) 	= join(X10,join(X11,X12))].
% 0.83/1.21  [464=param(411,261),[396],
% 0.83/1.21  			join(meet(X10,X11),X12) 	= join(meet(X11,X10),X12)].
% 0.83/1.21  [469=param(464,29),[392],
% 0.83/1.21  			join(meet(X10,X11),X12) 	= join(X12,meet(X11,X10))].
% 0.83/1.21  [542=param(207,11),[],
% 0.83/1.21  			join(meet(X10,X11),meet(meet(X12,X10),X11)) 	= meet(X10,X11)].
% 0.83/1.21  [554=param(221,11),[],
% 0.83/1.21  			join(meet(X10,X11),meet(X10,meet(X11,X12))) 	= meet(X10,X11)].
% 0.83/1.21  [557=param(554,69),[-469,542],
% 0.83/1.21  			meet(meet(X12,X10),meet(X11,X12)) 	= meet(X10,meet(X11,X12))].
% 0.83/1.21  [558=demod(367),[557],
% 0.83/1.21  			meet(meet(X10,X11),meet(X10,X12)) 	= meet(X12,meet(X10,X11))].
% 0.83/1.21  [564=param(554,71),[-469,542],
% 0.83/1.21  			meet(meet(X11,X10),meet(X11,X12)) 	= meet(X10,meet(X11,X12))].
% 0.83/1.21  [569=demod(558),[564],
% 0.83/1.21  			meet(X10,meet(X11,X12)) 	= meet(X12,meet(X11,X10))].
% 0.83/1.21  [590=demod(557),[],
% 0.83/1.21  			meet(meet(X10,X11),meet(X12,X10)) 	= meet(X11,meet(X12,X10))].
% 0.83/1.21  [593=demod(289),[],
% 0.83/1.21  			meet(meet(X10,X11),meet(join(X12,X10),X11)) 	= meet(X10,X11)].
% 0.83/1.21  [608=param(590,269),[],
% 0.83/1.21  			meet(meet(X10,X11),meet(X12,X11)) 	= meet(X10,meet(X12,X11))].
% 0.83/1.21  [613=demod(564),[],
% 0.83/1.21  			meet(meet(X10,X11),meet(X10,X12)) 	= meet(X11,meet(X10,X12))].
% 0.83/1.21  [620=demod(593),[608],
% 0.83/1.21  			meet(X10,meet(join(X11,X10),X12)) 	= meet(X10,X12)].
% 0.83/1.21  [633=param(620,12),[613],
% 0.83/1.21  			meet(meet(X11,X10),X12) 	= meet(X10,meet(X11,X12))].
% 0.83/1.21  [652=param(6,633),[269,269,569,5],
% 0.83/1.21  			thmtrue 	= thmfalse].
% 0.83/1.21  % SZS output end CNFRefutation
% 0.83/1.21  Space:    594 KB 
%------------------------------------------------------------------------------