%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWV396+1 : TPTP v9.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n015.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 9 09:30:24 PM UTC 2025
% Result : Theorem 15.57s 4.87s
% Output : CNFRefutation 15.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 14
% Syntax : Number of formulae : 118 ( 59 unt; 0 typ; 0 def)
% Number of atoms : 229 ( 59 equ)
% Maximal formula atoms : 8 ( 1 avg)
% Number of connectives : 198 ( 87 ~; 88 |; 10 &)
% ( 4 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 25 ( 25 usr; 10 con; 0-3 aty)
% Number of variables : 173 ( 173 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ pair_in_list > succ_cpq > strictly_less_than > less_than > contains_slb > contains_cpq > ok > isnonempty_slb > check_cpq > triple > update_slb > remove_slb > remove_pqp > remove_cpq > pair > lookup_slb > insert_slb > insert_pqp > insert_cpq > #nlpp > removemin_cpq_res > removemin_cpq_eff > findmin_pqp_res > findmin_cpq_res > findmin_cpq_eff > create_slb > bottom > bad > #skF_7 > #skF_5 > #skF_6 > #skF_2 > #skF_3 > #skF_1 > #skF_4
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(bad,type,
bad: $i ).
tff(insert_cpq,type,
insert_cpq: ( $i * $i ) > $i ).
tff(succ_cpq,type,
succ_cpq: ( $i * $i ) > $o ).
tff(remove_cpq,type,
remove_cpq: ( $i * $i ) > $i ).
tff(contains_slb,type,
contains_slb: ( $i * $i ) > $o ).
tff(lookup_slb,type,
lookup_slb: ( $i * $i ) > $i ).
tff('#skF_7',type,
'#skF_7': $i ).
tff(pair_in_list,type,
pair_in_list: ( $i * $i * $i ) > $o ).
tff('#skF_5',type,
'#skF_5': $i ).
tff(less_than,type,
less_than: ( $i * $i ) > $o ).
tff('#skF_6',type,
'#skF_6': $i ).
tff('#skF_2',type,
'#skF_2': $i ).
tff('#skF_3',type,
'#skF_3': $i ).
tff('#skF_1',type,
'#skF_1': $i ).
tff(contains_cpq,type,
contains_cpq: ( $i * $i ) > $o ).
tff(strictly_less_than,type,
strictly_less_than: ( $i * $i ) > $o ).
tff(pair,type,
pair: ( $i * $i ) > $i ).
tff(ok,type,
ok: $i > $o ).
tff(insert_pqp,type,
insert_pqp: ( $i * $i ) > $i ).
tff(findmin_pqp_res,type,
findmin_pqp_res: $i > $i ).
tff(remove_pqp,type,
remove_pqp: ( $i * $i ) > $i ).
tff(bottom,type,
bottom: $i ).
tff(triple,type,
triple: ( $i * $i * $i ) > $i ).
tff(removemin_cpq_res,type,
removemin_cpq_res: $i > $i ).
tff('#skF_4',type,
'#skF_4': $i ).
tff(isnonempty_slb,type,
isnonempty_slb: $i > $o ).
tff(check_cpq,type,
check_cpq: $i > $o ).
tff(remove_slb,type,
remove_slb: ( $i * $i ) > $i ).
tff(findmin_cpq_eff,type,
findmin_cpq_eff: $i > $i ).
tff(removemin_cpq_eff,type,
removemin_cpq_eff: $i > $i ).
tff(create_slb,type,
create_slb: $i ).
tff(findmin_cpq_res,type,
findmin_cpq_res: $i > $i ).
tff(insert_slb,type,
insert_slb: ( $i * $i ) > $i ).
tff(update_slb,type,
update_slb: ( $i * $i ) > $i ).
tff(f_110,axiom,
! [U,V,W,X] :
( contains_slb(insert_slb(U,pair(V,X)),W)
<=> ( contains_slb(U,W)
| ( V = W ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+2.ax',ax21) ).
tff(f_306,negated_conjecture,
~ ! [U] :
( ! [V,W,X,Y] :
( ( pair_in_list(U,X,Y)
& strictly_less_than(X,Y)
& ok(remove_cpq(triple(V,U,W),X)) )
=> pair_in_list(remove_slb(U,X),X,Y) )
=> ! [Z,X1,X2,X3,X4,X5] :
( ( pair_in_list(insert_slb(U,pair(X4,X5)),X2,X3)
& strictly_less_than(X2,X3)
& ok(remove_cpq(triple(Z,insert_slb(U,pair(X4,X5)),X1),X2)) )
=> pair_in_list(remove_slb(insert_slb(U,pair(X4,X5)),X2),X2,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l32_co) ).
tff(f_132,axiom,
! [U,V,W] : ( lookup_slb(insert_slb(U,pair(V,W)),V) = W ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+2.ax',ax26) ).
tff(f_123,axiom,
! [U,V,W] : ( remove_slb(insert_slb(U,pair(V,W)),V) = U ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+2.ax',ax24) ).
tff(f_121,axiom,
! [U,V,W,X,Y] :
( pair_in_list(insert_slb(U,pair(V,X)),W,Y)
<=> ( pair_in_list(U,W,Y)
| ( ( V = W )
& ( X = Y ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+2.ax',ax23) ).
tff(f_69,axiom,
! [U,V] :
( strictly_less_than(U,V)
<=> ( less_than(U,V)
& ~ less_than(V,U) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+0.ax',stricly_smaller_definition) ).
tff(f_217,axiom,
! [U,V] :
( ok(triple(U,V,bad))
<=> $false ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax40) ).
tff(f_229,axiom,
! [U,V,W,X] :
( ~ contains_slb(V,X)
=> ( remove_cpq(triple(U,V,W),X) = triple(U,V,bad) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax43) ).
tff(f_139,axiom,
! [U,V,W,X] :
( ( ( V != W )
& contains_slb(U,W) )
=> ( lookup_slb(insert_slb(U,pair(V,X)),W) = lookup_slb(U,W) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+2.ax',ax27) ).
tff(f_241,axiom,
! [U,V,W,X] :
( ( contains_slb(V,X)
& strictly_less_than(X,lookup_slb(V,X)) )
=> ( remove_cpq(triple(U,V,W),X) = triple(remove_pqp(U,X),remove_slb(V,X),bad) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax45) ).
tff(f_60,axiom,
! [U,V] :
( less_than(U,V)
| less_than(V,U) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+0.ax',totality) ).
tff(f_235,axiom,
! [U,V,W,X] :
( ( contains_slb(V,X)
& less_than(lookup_slb(V,X),X) )
=> ( remove_cpq(triple(U,V,W),X) = triple(remove_pqp(U,X),remove_slb(V,X),W) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax44) ).
tff(f_222,axiom,
! [U,V,W] :
( ~ ok(triple(U,V,W))
=> ( W = bad ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax41) ).
tff(f_130,axiom,
! [U,V,W,X] :
( ( ( V != W )
& contains_slb(U,W) )
=> ( remove_slb(insert_slb(U,pair(V,X)),W) = insert_slb(remove_slb(U,W),pair(V,X)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+2.ax',ax25) ).
tff(c_24,plain,
! [U_14,W_16,X_17] : contains_slb(insert_slb(U_14,pair(W_16,X_17)),W_16),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_106,plain,
strictly_less_than('#skF_4','#skF_5'),
inference(cnfTransformation,[status(thm)],[f_306]) ).
tff(c_42,plain,
! [U_32,V_33,W_34] : ( lookup_slb(insert_slb(U_32,pair(V_33,W_34)),V_33) = W_34 ),
inference(cnfTransformation,[status(thm)],[f_132]) ).
tff(c_38,plain,
! [U_25,V_26,W_27] : ( remove_slb(insert_slb(U_25,pair(V_26,W_27)),V_26) = U_25 ),
inference(cnfTransformation,[status(thm)],[f_123]) ).
tff(c_108,plain,
pair_in_list(insert_slb('#skF_1',pair('#skF_6','#skF_7')),'#skF_4','#skF_5'),
inference(cnfTransformation,[status(thm)],[f_306]) ).
tff(c_1080,plain,
! [Y_265,V_264,U_263,X_266,W_267] :
( ( W_267 = V_264 )
| pair_in_list(U_263,W_267,Y_265)
| ~ pair_in_list(insert_slb(U_263,pair(V_264,X_266)),W_267,Y_265) ),
inference(cnfTransformation,[status(thm)],[f_121]) ).
tff(c_1093,plain,
( ( '#skF_6' = '#skF_4' )
| pair_in_list('#skF_1','#skF_4','#skF_5') ),
inference(resolution,[status(thm)],[c_108,c_1080]) ).
tff(c_1094,plain,
pair_in_list('#skF_1','#skF_4','#skF_5'),
inference(splitLeft,[status(thm)],[c_1093]) ).
tff(c_147,plain,
! [V_151,U_152] :
( ~ less_than(V_151,U_152)
| ~ strictly_less_than(U_152,V_151) ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_151,plain,
~ less_than('#skF_5','#skF_4'),
inference(resolution,[status(thm)],[c_106,c_147]) ).
tff(c_74,plain,
! [U_75,V_76] : ~ ok(triple(U_75,V_76,bad)),
inference(cnfTransformation,[status(thm)],[f_217]) ).
tff(c_835,plain,
! [U_250,V_251,W_252,X_253] :
( ( remove_cpq(triple(U_250,V_251,W_252),X_253) = triple(U_250,V_251,bad) )
| contains_slb(V_251,X_253) ),
inference(cnfTransformation,[status(thm)],[f_229]) ).
tff(c_104,plain,
ok(remove_cpq(triple('#skF_2',insert_slb('#skF_1',pair('#skF_6','#skF_7')),'#skF_3'),'#skF_4')),
inference(cnfTransformation,[status(thm)],[f_306]) ).
tff(c_848,plain,
( ok(triple('#skF_2',insert_slb('#skF_1',pair('#skF_6','#skF_7')),bad))
| contains_slb(insert_slb('#skF_1',pair('#skF_6','#skF_7')),'#skF_4') ),
inference(superposition,[status(thm),theory(equality)],[c_835,c_104]) ).
tff(c_860,plain,
contains_slb(insert_slb('#skF_1',pair('#skF_6','#skF_7')),'#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_74,c_848]) ).
tff(c_22,plain,
! [W_16,V_15,U_14,X_17] :
( ( W_16 = V_15 )
| contains_slb(U_14,W_16)
| ~ contains_slb(insert_slb(U_14,pair(V_15,X_17)),W_16) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_866,plain,
( ( '#skF_6' = '#skF_4' )
| contains_slb('#skF_1','#skF_4') ),
inference(resolution,[status(thm)],[c_860,c_22]) ).
tff(c_867,plain,
contains_slb('#skF_1','#skF_4'),
inference(splitLeft,[status(thm)],[c_866]) ).
tff(c_44,plain,
! [U_35,V_36,X_38,W_37] :
( ( lookup_slb(insert_slb(U_35,pair(V_36,X_38)),W_37) = lookup_slb(U_35,W_37) )
| ~ contains_slb(U_35,W_37)
| ( W_37 = V_36 ) ),
inference(cnfTransformation,[status(thm)],[f_139]) ).
tff(c_142,plain,
! [U_149,V_150] :
( less_than(U_149,V_150)
| ~ strictly_less_than(U_149,V_150) ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_146,plain,
less_than('#skF_4','#skF_5'),
inference(resolution,[status(thm)],[c_106,c_142]) ).
tff(c_8,plain,
! [U_7,V_8] :
( strictly_less_than(U_7,V_8)
| less_than(V_8,U_7)
| ~ less_than(U_7,V_8) ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_4244,plain,
! [U_521,X_522,V_523,W_524] :
( ( triple(remove_pqp(U_521,X_522),remove_slb(V_523,X_522),bad) = remove_cpq(triple(U_521,V_523,W_524),X_522) )
| ~ strictly_less_than(X_522,lookup_slb(V_523,X_522))
| ~ contains_slb(V_523,X_522) ),
inference(cnfTransformation,[status(thm)],[f_241]) ).
tff(c_4372,plain,
! [U_525,V_526,W_527,X_528] :
( ~ ok(remove_cpq(triple(U_525,V_526,W_527),X_528))
| ~ strictly_less_than(X_528,lookup_slb(V_526,X_528))
| ~ contains_slb(V_526,X_528) ),
inference(superposition,[status(thm),theory(equality)],[c_4244,c_74]) ).
tff(c_4388,plain,
( ~ strictly_less_than('#skF_4',lookup_slb(insert_slb('#skF_1',pair('#skF_6','#skF_7')),'#skF_4'))
| ~ contains_slb(insert_slb('#skF_1',pair('#skF_6','#skF_7')),'#skF_4') ),
inference(resolution,[status(thm)],[c_104,c_4372]) ).
tff(c_4391,plain,
~ strictly_less_than('#skF_4',lookup_slb(insert_slb('#skF_1',pair('#skF_6','#skF_7')),'#skF_4')),
inference(demodulation,[status(thm),theory(equality)],[c_860,c_4388]) ).
tff(c_4400,plain,
( less_than(lookup_slb(insert_slb('#skF_1',pair('#skF_6','#skF_7')),'#skF_4'),'#skF_4')
| ~ less_than('#skF_4',lookup_slb(insert_slb('#skF_1',pair('#skF_6','#skF_7')),'#skF_4')) ),
inference(resolution,[status(thm)],[c_8,c_4391]) ).
tff(c_4402,plain,
~ less_than('#skF_4',lookup_slb(insert_slb('#skF_1',pair('#skF_6','#skF_7')),'#skF_4')),
inference(splitLeft,[status(thm)],[c_4400]) ).
tff(c_4418,plain,
( ~ less_than('#skF_4',lookup_slb('#skF_1','#skF_4'))
| ~ contains_slb('#skF_1','#skF_4')
| ( '#skF_6' = '#skF_4' ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_4402]) ).
tff(c_4435,plain,
( ~ less_than('#skF_4',lookup_slb('#skF_1','#skF_4'))
| ( '#skF_6' = '#skF_4' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_867,c_4418]) ).
tff(c_4436,plain,
~ less_than('#skF_4',lookup_slb('#skF_1','#skF_4')),
inference(splitLeft,[status(thm)],[c_4435]) ).
tff(c_4,plain,
! [V_5,U_4] :
( less_than(V_5,U_4)
| less_than(U_4,V_5) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_4014,plain,
! [U_502,X_503,V_504,W_505] :
( ( triple(remove_pqp(U_502,X_503),remove_slb(V_504,X_503),W_505) = remove_cpq(triple(U_502,V_504,W_505),X_503) )
| ~ less_than(lookup_slb(V_504,X_503),X_503)
| ~ contains_slb(V_504,X_503) ),
inference(cnfTransformation,[status(thm)],[f_235]) ).
tff(c_76,plain,
! [W_79,U_77,V_78] :
( ( bad = W_79 )
| ok(triple(U_77,V_78,W_79)) ),
inference(cnfTransformation,[status(thm)],[f_222]) ).
tff(c_6202,plain,
! [W_602,U_603,V_604,X_605] :
( ( bad = W_602 )
| ok(remove_cpq(triple(U_603,V_604,W_602),X_605))
| ~ less_than(lookup_slb(V_604,X_605),X_605)
| ~ contains_slb(V_604,X_605) ),
inference(superposition,[status(thm),theory(equality)],[c_4014,c_76]) ).
tff(c_6591,plain,
! [W_658,U_659,V_660,V_661] :
( ( bad = W_658 )
| ok(remove_cpq(triple(U_659,V_660,W_658),V_661))
| ~ contains_slb(V_660,V_661)
| less_than(V_661,lookup_slb(V_660,V_661)) ),
inference(resolution,[status(thm)],[c_4,c_6202]) ).
tff(c_110,plain,
! [X_130,Y_131,V_128,W_129] :
( pair_in_list(remove_slb('#skF_1',X_130),X_130,Y_131)
| ~ ok(remove_cpq(triple(V_128,'#skF_1',W_129),X_130))
| ~ strictly_less_than(X_130,Y_131)
| ~ pair_in_list('#skF_1',X_130,Y_131) ),
inference(cnfTransformation,[status(thm)],[f_306]) ).
tff(c_6657,plain,
! [V_661,Y_131,W_658] :
( pair_in_list(remove_slb('#skF_1',V_661),V_661,Y_131)
| ~ strictly_less_than(V_661,Y_131)
| ~ pair_in_list('#skF_1',V_661,Y_131)
| ( bad = W_658 )
| ~ contains_slb('#skF_1',V_661)
| less_than(V_661,lookup_slb('#skF_1',V_661)) ),
inference(resolution,[status(thm)],[c_6591,c_110]) ).
tff(c_7584,plain,
! [V_825,Y_826] :
( pair_in_list(remove_slb('#skF_1',V_825),V_825,Y_826)
| ~ strictly_less_than(V_825,Y_826)
| ~ pair_in_list('#skF_1',V_825,Y_826)
| ~ contains_slb('#skF_1',V_825)
| less_than(V_825,lookup_slb('#skF_1',V_825)) ),
inference(splitLeft,[status(thm)],[c_6657]) ).
tff(c_36,plain,
! [V_21,U_20,Y_24,X_23,W_22] :
( ~ pair_in_list(U_20,W_22,Y_24)
| pair_in_list(insert_slb(U_20,pair(V_21,X_23)),W_22,Y_24) ),
inference(cnfTransformation,[status(thm)],[f_121]) ).
tff(c_3148,plain,
! [U_483,V_484,X_485,W_486] :
( ( remove_slb(insert_slb(U_483,pair(V_484,X_485)),W_486) = insert_slb(remove_slb(U_483,W_486),pair(V_484,X_485)) )
| ~ contains_slb(U_483,W_486)
| ( W_486 = V_484 ) ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_102,plain,
~ pair_in_list(remove_slb(insert_slb('#skF_1',pair('#skF_6','#skF_7')),'#skF_4'),'#skF_4','#skF_5'),
inference(cnfTransformation,[status(thm)],[f_306]) ).
tff(c_3158,plain,
( ~ pair_in_list(insert_slb(remove_slb('#skF_1','#skF_4'),pair('#skF_6','#skF_7')),'#skF_4','#skF_5')
| ~ contains_slb('#skF_1','#skF_4')
| ( '#skF_6' = '#skF_4' ) ),
inference(superposition,[status(thm),theory(equality)],[c_3148,c_102]) ).
tff(c_3171,plain,
( ~ pair_in_list(insert_slb(remove_slb('#skF_1','#skF_4'),pair('#skF_6','#skF_7')),'#skF_4','#skF_5')
| ( '#skF_6' = '#skF_4' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_867,c_3158]) ).
tff(c_3174,plain,
~ pair_in_list(insert_slb(remove_slb('#skF_1','#skF_4'),pair('#skF_6','#skF_7')),'#skF_4','#skF_5'),
inference(splitLeft,[status(thm)],[c_3171]) ).
tff(c_3178,plain,
~ pair_in_list(remove_slb('#skF_1','#skF_4'),'#skF_4','#skF_5'),
inference(resolution,[status(thm)],[c_36,c_3174]) ).
tff(c_7587,plain,
( ~ strictly_less_than('#skF_4','#skF_5')
| ~ pair_in_list('#skF_1','#skF_4','#skF_5')
| ~ contains_slb('#skF_1','#skF_4')
| less_than('#skF_4',lookup_slb('#skF_1','#skF_4')) ),
inference(resolution,[status(thm)],[c_7584,c_3178]) ).
tff(c_7590,plain,
less_than('#skF_4',lookup_slb('#skF_1','#skF_4')),
inference(demodulation,[status(thm),theory(equality)],[c_867,c_1094,c_106,c_7587]) ).
tff(c_7592,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_4436,c_7590]) ).
tff(c_7595,plain,
bad = '#skF_5',
inference(splitRight,[status(thm)],[c_6657]) ).
tff(c_7593,plain,
! [W_658] : ( bad = W_658 ),
inference(splitRight,[status(thm)],[c_6657]) ).
tff(c_8347,plain,
! [W_4519] : ( W_4519 = '#skF_5' ),
inference(superposition,[status(thm),theory(equality)],[c_7595,c_7593]) ).
tff(c_8514,plain,
~ less_than('#skF_4','#skF_5'),
inference(superposition,[status(thm),theory(equality)],[c_8347,c_4436]) ).
tff(c_9180,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_146,c_8514]) ).
tff(c_9181,plain,
'#skF_6' = '#skF_4',
inference(splitRight,[status(thm)],[c_4435]) ).
tff(c_9188,plain,
~ pair_in_list(remove_slb(insert_slb('#skF_1',pair('#skF_4','#skF_7')),'#skF_4'),'#skF_4','#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_9181,c_102]) ).
tff(c_9195,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1094,c_38,c_9188]) ).
tff(c_9196,plain,
less_than(lookup_slb(insert_slb('#skF_1',pair('#skF_6','#skF_7')),'#skF_4'),'#skF_4'),
inference(splitRight,[status(thm)],[c_4400]) ).
tff(c_9226,plain,
( less_than(lookup_slb('#skF_1','#skF_4'),'#skF_4')
| ~ contains_slb('#skF_1','#skF_4')
| ( '#skF_6' = '#skF_4' ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_9196]) ).
tff(c_9243,plain,
( less_than(lookup_slb('#skF_1','#skF_4'),'#skF_4')
| ( '#skF_6' = '#skF_4' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_867,c_9226]) ).
tff(c_9260,plain,
'#skF_6' = '#skF_4',
inference(splitLeft,[status(thm)],[c_9243]) ).
tff(c_9266,plain,
~ pair_in_list(remove_slb(insert_slb('#skF_1',pair('#skF_4','#skF_7')),'#skF_4'),'#skF_4','#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_9260,c_102]) ).
tff(c_9273,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1094,c_38,c_9266]) ).
tff(c_9274,plain,
less_than(lookup_slb('#skF_1','#skF_4'),'#skF_4'),
inference(splitRight,[status(thm)],[c_9243]) ).
tff(c_13263,plain,
! [W_8275,U_8276,V_8277,X_8278] :
( ( bad = W_8275 )
| ok(remove_cpq(triple(U_8276,V_8277,W_8275),X_8278))
| ~ less_than(lookup_slb(V_8277,X_8278),X_8278)
| ~ contains_slb(V_8277,X_8278) ),
inference(superposition,[status(thm),theory(equality)],[c_4014,c_76]) ).
tff(c_13322,plain,
! [W_8275,U_8276] :
( ( bad = W_8275 )
| ok(remove_cpq(triple(U_8276,'#skF_1',W_8275),'#skF_4'))
| ~ contains_slb('#skF_1','#skF_4') ),
inference(resolution,[status(thm)],[c_9274,c_13263]) ).
tff(c_13466,plain,
! [W_8279,U_8280] :
( ( bad = W_8279 )
| ok(remove_cpq(triple(U_8280,'#skF_1',W_8279),'#skF_4')) ),
inference(demodulation,[status(thm),theory(equality)],[c_867,c_13322]) ).
tff(c_13489,plain,
! [Y_131,W_8279] :
( pair_in_list(remove_slb('#skF_1','#skF_4'),'#skF_4',Y_131)
| ~ strictly_less_than('#skF_4',Y_131)
| ~ pair_in_list('#skF_1','#skF_4',Y_131)
| ( bad = W_8279 ) ),
inference(resolution,[status(thm)],[c_13466,c_110]) ).
tff(c_13606,plain,
bad = '#skF_5',
inference(splitLeft,[status(thm)],[c_13489]) ).
tff(c_13601,plain,
! [W_8279] : ( bad = W_8279 ),
inference(splitLeft,[status(thm)],[c_13489]) ).
tff(c_15133,plain,
! [W_16136] : ( W_16136 = '#skF_5' ),
inference(superposition,[status(thm),theory(equality)],[c_13606,c_13601]) ).
tff(c_15334,plain,
less_than('#skF_5','#skF_4'),
inference(superposition,[status(thm),theory(equality)],[c_15133,c_9274]) ).
tff(c_16021,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_151,c_15334]) ).
tff(c_16385,plain,
! [Y_20146] :
( pair_in_list(remove_slb('#skF_1','#skF_4'),'#skF_4',Y_20146)
| ~ strictly_less_than('#skF_4',Y_20146)
| ~ pair_in_list('#skF_1','#skF_4',Y_20146) ),
inference(splitRight,[status(thm)],[c_13489]) ).
tff(c_16388,plain,
( ~ strictly_less_than('#skF_4','#skF_5')
| ~ pair_in_list('#skF_1','#skF_4','#skF_5') ),
inference(resolution,[status(thm)],[c_16385,c_3178]) ).
tff(c_16392,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1094,c_106,c_16388]) ).
tff(c_16393,plain,
'#skF_6' = '#skF_4',
inference(splitRight,[status(thm)],[c_3171]) ).
tff(c_16397,plain,
~ pair_in_list(remove_slb(insert_slb('#skF_1',pair('#skF_4','#skF_7')),'#skF_4'),'#skF_4','#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_16393,c_102]) ).
tff(c_16402,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1094,c_38,c_16397]) ).
tff(c_16404,plain,
~ pair_in_list('#skF_1','#skF_4','#skF_5'),
inference(splitRight,[status(thm)],[c_1093]) ).
tff(c_16403,plain,
'#skF_6' = '#skF_4',
inference(splitRight,[status(thm)],[c_1093]) ).
tff(c_16408,plain,
pair_in_list(insert_slb('#skF_1',pair('#skF_4','#skF_7')),'#skF_4','#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_16403,c_108]) ).
tff(c_16422,plain,
! [V_20148,U_20147,X_20150,Y_20149,W_20151] :
( ( Y_20149 = X_20150 )
| pair_in_list(U_20147,W_20151,Y_20149)
| ~ pair_in_list(insert_slb(U_20147,pair(V_20148,X_20150)),W_20151,Y_20149) ),
inference(cnfTransformation,[status(thm)],[f_121]) ).
tff(c_16425,plain,
( ( '#skF_7' = '#skF_5' )
| pair_in_list('#skF_1','#skF_4','#skF_5') ),
inference(resolution,[status(thm)],[c_16408,c_16422]) ).
tff(c_16434,plain,
'#skF_7' = '#skF_5',
inference(negUnitSimplification,[status(thm)],[c_16404,c_16425]) ).
tff(c_16406,plain,
ok(remove_cpq(triple('#skF_2',insert_slb('#skF_1',pair('#skF_4','#skF_7')),'#skF_3'),'#skF_4')),
inference(demodulation,[status(thm),theory(equality)],[c_16403,c_104]) ).
tff(c_16449,plain,
ok(remove_cpq(triple('#skF_2',insert_slb('#skF_1',pair('#skF_4','#skF_5')),'#skF_3'),'#skF_4')),
inference(demodulation,[status(thm),theory(equality)],[c_16434,c_16406]) ).
tff(c_18456,plain,
! [U_20363,X_20364,V_20365,W_20366] :
( ( triple(remove_pqp(U_20363,X_20364),remove_slb(V_20365,X_20364),bad) = remove_cpq(triple(U_20363,V_20365,W_20366),X_20364) )
| ~ strictly_less_than(X_20364,lookup_slb(V_20365,X_20364))
| ~ contains_slb(V_20365,X_20364) ),
inference(cnfTransformation,[status(thm)],[f_241]) ).
tff(c_18568,plain,
! [U_20367,V_20368,W_20369,X_20370] :
( ~ ok(remove_cpq(triple(U_20367,V_20368,W_20369),X_20370))
| ~ strictly_less_than(X_20370,lookup_slb(V_20368,X_20370))
| ~ contains_slb(V_20368,X_20370) ),
inference(superposition,[status(thm),theory(equality)],[c_18456,c_74]) ).
tff(c_18578,plain,
( ~ strictly_less_than('#skF_4',lookup_slb(insert_slb('#skF_1',pair('#skF_4','#skF_5')),'#skF_4'))
| ~ contains_slb(insert_slb('#skF_1',pair('#skF_4','#skF_5')),'#skF_4') ),
inference(resolution,[status(thm)],[c_16449,c_18568]) ).
tff(c_18586,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_24,c_106,c_42,c_18578]) ).
tff(c_18587,plain,
'#skF_6' = '#skF_4',
inference(splitRight,[status(thm)],[c_866]) ).
tff(c_18591,plain,
~ pair_in_list(remove_slb(insert_slb('#skF_1',pair('#skF_4','#skF_7')),'#skF_4'),'#skF_4','#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_18587,c_102]) ).
tff(c_18594,plain,
~ pair_in_list('#skF_1','#skF_4','#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_18591]) ).
tff(c_18592,plain,
pair_in_list(insert_slb('#skF_1',pair('#skF_4','#skF_7')),'#skF_4','#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_18587,c_108]) ).
tff(c_19099,plain,
! [W_20399,U_20395,X_20398,Y_20397,V_20396] :
( ( Y_20397 = X_20398 )
| pair_in_list(U_20395,W_20399,Y_20397)
| ~ pair_in_list(insert_slb(U_20395,pair(V_20396,X_20398)),W_20399,Y_20397) ),
inference(cnfTransformation,[status(thm)],[f_121]) ).
tff(c_19102,plain,
( ( '#skF_7' = '#skF_5' )
| pair_in_list('#skF_1','#skF_4','#skF_5') ),
inference(resolution,[status(thm)],[c_18592,c_19099]) ).
tff(c_19111,plain,
'#skF_7' = '#skF_5',
inference(negUnitSimplification,[status(thm)],[c_18594,c_19102]) ).
tff(c_18590,plain,
ok(remove_cpq(triple('#skF_2',insert_slb('#skF_1',pair('#skF_4','#skF_7')),'#skF_3'),'#skF_4')),
inference(demodulation,[status(thm),theory(equality)],[c_18587,c_104]) ).
tff(c_19115,plain,
ok(remove_cpq(triple('#skF_2',insert_slb('#skF_1',pair('#skF_4','#skF_5')),'#skF_3'),'#skF_4')),
inference(demodulation,[status(thm),theory(equality)],[c_19111,c_18590]) ).
tff(c_21192,plain,
! [U_20621,X_20622,V_20623,W_20624] :
( ( triple(remove_pqp(U_20621,X_20622),remove_slb(V_20623,X_20622),bad) = remove_cpq(triple(U_20621,V_20623,W_20624),X_20622) )
| ~ strictly_less_than(X_20622,lookup_slb(V_20623,X_20622))
| ~ contains_slb(V_20623,X_20622) ),
inference(cnfTransformation,[status(thm)],[f_241]) ).
tff(c_21308,plain,
! [U_20625,V_20626,W_20627,X_20628] :
( ~ ok(remove_cpq(triple(U_20625,V_20626,W_20627),X_20628))
| ~ strictly_less_than(X_20628,lookup_slb(V_20626,X_20628))
| ~ contains_slb(V_20626,X_20628) ),
inference(superposition,[status(thm),theory(equality)],[c_21192,c_74]) ).
tff(c_21318,plain,
( ~ strictly_less_than('#skF_4',lookup_slb(insert_slb('#skF_1',pair('#skF_4','#skF_5')),'#skF_4'))
| ~ contains_slb(insert_slb('#skF_1',pair('#skF_4','#skF_5')),'#skF_4') ),
inference(resolution,[status(thm)],[c_19115,c_21308]) ).
tff(c_21326,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_24,c_106,c_42,c_21318]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWV396+1 : TPTP v9.0.0. Released v3.3.0.
% 0.03/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.14/0.34 % Computer : n015.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed Apr 9 03:11:20 EDT 2025
% 0.14/0.34 % CPUTime :
% 15.57/4.87 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.57/4.88
% 15.57/4.88 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------