↑ Up

Fiesta---2.UNS-CRf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Fiesta---2
% Problem  : LCL416-10 : TPTP v8.1.0. Released v7.3.0.
% Transfm  : none
% Format   : dedam
% Command  : fiesta-wrapper %s

% Computer : n021.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 10:35:23 EDT 2022

% Result   : Unsatisfiable 3.67s 4.04s
% Output   : CNFRefutation 3.67s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12  % Problem  : LCL416-10 : TPTP v8.1.0. Released v7.3.0.
% 0.08/0.13  % Command  : fiesta-wrapper %s
% 0.13/0.34  % Computer : n021.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % WCLimit  : 600
% 0.13/0.34  % DateTime : Mon Jul  4 08:54:16 EDT 2022
% 0.13/0.34  % CPUTime  : 
% 3.67/4.04  Theorem Proved.
% 3.67/4.04  % SZS status Unsatisfiable
% 3.67/4.04  % SZS output start CNFRefutation
% 3.67/4.04  [1=axiom,[],
% 3.67/4.04  			is_a_theorem(equivalent(X10,equivalent(equivalent(equivalent(X10,X11),equivalent(X12,X11)),X12))) 	= true].
% 3.67/4.04  [2=axiom,[],
% 3.67/4.04  			ifeq(is_a_theorem(equivalent(X10,X11)),true,ifeq(is_a_theorem(X10),true,is_a_theorem(X11),true),true) 	= true].
% 3.67/4.04  [3=axiom,[],
% 3.67/4.04  			ifeq(X10,X10,X11,X12) 	= X11].
% 3.67/4.04  [4=axiom,[],
% 3.67/4.04  			thtop(X10,X10) 	= thmfalse].
% 3.67/4.04  [5=axiom,[],
% 3.67/4.04  			thtop(is_a_theorem(equivalent(a,a)),true) 	= thmtrue].
% 3.67/4.04  [6=param(2,1),[3],
% 3.67/4.04  			ifeq(is_a_theorem(X10),true,is_a_theorem(equivalent(equivalent(equivalent(X10,X11),equivalent(X12,X11)),X12)),true) 	= true].
% 3.67/4.04  [7=param(2,1),[3],
% 3.67/4.04  			ifeq(is_a_theorem(equivalent(equivalent(X10,equivalent(equivalent(equivalent(X10,X11),equivalent(X12,X11)),X12)),X13)),true,is_a_theorem(X13),true) 	= true].
% 3.67/4.04  [8=param(6,1),[3],
% 3.67/4.04  			is_a_theorem(equivalent(equivalent(equivalent(equivalent(X10,equivalent(equivalent(equivalent(X10,X11),equivalent(X12,X11)),X12)),X13),equivalent(X14,X13)),X14)) 	= true].
% 3.67/4.04  [10=param(7,8),[3],
% 3.67/4.04  			is_a_theorem(equivalent(equivalent(equivalent(equivalent(X10,equivalent(equivalent(equivalent(X10,X11),equivalent(X12,X11)),X12)),X13),X14),equivalent(X13,X14))) 	= true].
% 3.67/4.04  [12=param(2,8),[3],
% 3.67/4.04  			ifeq(is_a_theorem(equivalent(equivalent(equivalent(X10,equivalent(equivalent(equivalent(X10,X11),equivalent(X12,X11)),X12)),X13),equivalent(X14,X13))),true,is_a_theorem(X14),true) 	= true].
% 3.67/4.04  [14=param(7,10),[3],
% 3.67/4.04  			is_a_theorem(equivalent(X10,equivalent(equivalent(equivalent(equivalent(equivalent(X11,equivalent(equivalent(equivalent(X11,X12),equivalent(X13,X12)),X13)),X10),X14),equivalent(X15,X14)),X15))) 	= true].
% 3.67/4.04  [17=param(2,10),[3],
% 3.67/4.04  			ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X10,equivalent(equivalent(equivalent(X10,X11),equivalent(X12,X11)),X12)),X13),X14),equivalent(X13,X14)),X15)),true,is_a_theorem(X15),true) 	= true].
% 3.67/4.04  [24=param(6,8),[3],
% 3.67/4.04  			is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X10,equivalent(equivalent(equivalent(X10,X11),equivalent(X12,X11)),X12)),X13),equivalent(X14,X13)),X14),X15),equivalent(X16,X15)),X16)) 	= true].
% 3.67/4.04  [28=param(7,24),[3],
% 3.67/4.04  			is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X10,equivalent(equivalent(equivalent(X10,X11),equivalent(X12,X11)),X12)),X13),equivalent(X14,X13)),X14),X15),X16),equivalent(X15,X16))) 	= true].
% 3.67/4.04  [46=param(2,28),[3],
% 3.67/4.04  			ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X10,equivalent(equivalent(equivalent(X10,X11),equivalent(X12,X11)),X12)),X13),equivalent(X14,X13)),X14),X15),X16)),true,is_a_theorem(equivalent(X15,X16)),true) 	= true].
% 3.67/4.04  [60=param(7,14),[3],
% 3.67/4.04  			is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X10,equivalent(equivalent(equivalent(X10,X11),equivalent(X12,X11)),X12)),equivalent(X13,equivalent(equivalent(equivalent(X13,X14),equivalent(X15,X14)),X15))),X16),equivalent(X17,X16)),X17)) 	= true].
% 3.67/4.04  [83=param(46,60),[3],
% 3.67/4.04  			is_a_theorem(equivalent(equivalent(X10,equivalent(X11,equivalent(equivalent(equivalent(X11,X12),equivalent(X13,X12)),X13))),X10)) 	= true].
% 3.67/4.04  [84=param(2,83),[3],
% 3.67/4.04  			ifeq(is_a_theorem(equivalent(X10,equivalent(X11,equivalent(equivalent(equivalent(X11,X12),equivalent(X13,X12)),X13)))),true,is_a_theorem(X10),true) 	= true].
% 3.67/4.04  [92=param(17,83),[3],
% 3.67/4.04  			is_a_theorem(equivalent(equivalent(equivalent(X10,equivalent(equivalent(equivalent(X10,X11),equivalent(X12,X11)),X12)),X13),equivalent(equivalent(equivalent(X13,X14),equivalent(X15,X14)),X15))) 	= true].
% 3.67/4.04  [103=param(12,92),[3],
% 3.67/4.04  			is_a_theorem(equivalent(equivalent(X10,X11),equivalent(X10,X11))) 	= true].
% 3.67/4.04  [107=param(6,103),[3],
% 3.67/4.04  			is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X10,X11),equivalent(X10,X11)),X12),equivalent(X13,X12)),X13)) 	= true].
% 3.67/4.04  [139=param(2,107),[3],
% 3.67/4.04  			ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(X10,X11),equivalent(X10,X11)),X12),equivalent(X13,X12))),true,is_a_theorem(X13),true) 	= true].
% 3.67/4.04  [142=param(6,107),[3],
% 3.67/4.04  			is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X10,X11),equivalent(X10,X11)),X12),equivalent(X13,X12)),X13),X14),equivalent(X15,X14)),X15)) 	= true].
% 3.67/4.05  [143=param(7,107),[3],
% 3.67/4.05  			is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X10,X11),equivalent(X10,X11)),X12),X13),equivalent(X12,X13))) 	= true].
% 3.67/4.05  [155=param(2,143),[3],
% 3.67/4.05  			ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(X10,X11),equivalent(X10,X11)),X12),X13)),true,is_a_theorem(equivalent(X12,X13)),true) 	= true].
% 3.67/4.05  [159=param(7,143),[3],
% 3.67/4.05  			is_a_theorem(equivalent(X10,equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X11,X12),equivalent(X11,X12)),X10),X13),equivalent(X14,X13)),X14))) 	= true].
% 3.67/4.05  [727=param(139,159),[3],
% 3.67/4.05  			is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X10,X11),equivalent(X10,X11)),equivalent(equivalent(equivalent(X12,X13),equivalent(X12,X13)),X14)),X15),equivalent(X14,X15))) 	= true].
% 3.67/4.05  [1361=param(84,727),[3],
% 3.67/4.05  			is_a_theorem(equivalent(equivalent(equivalent(equivalent(X10,X11),equivalent(X10,X11)),equivalent(equivalent(equivalent(X12,X13),equivalent(X12,X13)),X14)),equivalent(equivalent(equivalent(X14,X15),equivalent(X16,X15)),X16))) 	= true].
% 3.67/4.05  [3444=param(139,1361),[3],
% 3.67/4.05  			is_a_theorem(equivalent(equivalent(X10,X11),equivalent(equivalent(equivalent(equivalent(X12,X13),equivalent(X12,X13)),X10),X11))) 	= true].
% 3.67/4.05  [3448=param(6,3444),[3],
% 3.67/4.05  			is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X10,X11),equivalent(equivalent(equivalent(equivalent(X12,X13),equivalent(X12,X13)),X10),X11)),X14),equivalent(X15,X14)),X15)) 	= true].
% 3.67/4.05  [3544=param(7,3448),[3],
% 3.67/4.05  			is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X10,X11),equivalent(equivalent(equivalent(equivalent(X12,X13),equivalent(X12,X13)),X10),X11)),X14),X15),equivalent(X14,X15))) 	= true].
% 3.67/4.05  [3631=param(2,3544),[3],
% 3.67/4.05  			ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(X10,X11),equivalent(equivalent(equivalent(equivalent(X12,X13),equivalent(X12,X13)),X10),X11)),X14),X15)),true,is_a_theorem(equivalent(X14,X15)),true) 	= true].
% 3.67/4.05  [3684=param(3631,142),[3],
% 3.67/4.05  			is_a_theorem(equivalent(equivalent(X10,equivalent(equivalent(equivalent(equivalent(X11,X12),equivalent(X11,X12)),equivalent(equivalent(equivalent(equivalent(X13,X14),equivalent(X13,X14)),X15),equivalent(X16,X15))),X16)),X10)) 	= true].
% 3.67/4.05  [3790=param(7,3684),[3],
% 3.67/4.05  			is_a_theorem(equivalent(equivalent(equivalent(equivalent(X10,X11),equivalent(X10,X11)),X12),X12)) 	= true].
% 3.67/4.05  [3805=param(155,3790),[3],
% 3.67/4.05  			is_a_theorem(equivalent(X10,X10)) 	= true].
% 3.67/4.05  [3892=param(5,3805),[4],
% 3.67/4.05  			thmtrue 	= thmfalse].
% 3.67/4.05  % SZS output end CNFRefutation
% 3.67/4.05  Space:  46004 KB 
%------------------------------------------------------------------------------