%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : CSR064+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.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 : Thu May 9 17:18:32 EDT 2024
% Result : Theorem 0.52s 0.71s
% Output : Refutation 0.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : CSR064+1 : TPTP v8.1.2. Released v3.4.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n003.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 : 300
% 0.13/0.34 % DateTime : Thu May 9 01:16:38 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.52/0.71 % Version: 1.5
% 0.52/0.71 % SZS status Theorem
% 0.52/0.71 % SZS output start CNFRefutation
% 0.52/0.71 fof(just3,axiom,individual(f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just3)).
% 0.52/0.71 cnf(c233,plain,individual(f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))),inference(split_conjunct,[status(thm)],[just3])).
% 0.52/0.71 fof(just2,axiom,(![OBJ]:(~(individual(OBJ)&setorcollection(OBJ)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just2)).
% 0.52/0.71 fof(c234,plain,(![OBJ]:(~individual(OBJ)|~setorcollection(OBJ))),inference(fof_nnf,[status(thm)],[just2])).
% 0.52/0.71 fof(c235,plain,(![X143]:(~individual(X143)|~setorcollection(X143))),inference(variable_rename,[status(thm)],[c234])).
% 0.52/0.71 cnf(c236,plain,~individual(X145)|~setorcollection(X145),inference(split_conjunct,[status(thm)],[c235])).
% 0.52/0.71 fof(just41,axiom,(![INS]:(![ARG2]:(subsetof(INS,ARG2)=>setorcollection(INS)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just41)).
% 0.52/0.71 fof(c113,plain,(![INS]:(![ARG2]:(~subsetof(INS,ARG2)|setorcollection(INS)))),inference(fof_nnf,[status(thm)],[just41])).
% 0.52/0.71 fof(c114,plain,(![INS]:((![ARG2]:~subsetof(INS,ARG2))|setorcollection(INS))),inference(shift_quantors,[status(thm)],[c113])).
% 0.52/0.71 fof(c116,plain,(![X68]:(![X69]:(~subsetof(X68,X69)|setorcollection(X68)))),inference(shift_quantors,[status(thm)],[fof(c115,plain,(![X68]:((![X69]:~subsetof(X68,X69))|setorcollection(X68))),inference(variable_rename,[status(thm)],[c114])).])).
% 0.52/0.71 cnf(c117,plain,~subsetof(X187,X186)|setorcollection(X187),inference(split_conjunct,[status(thm)],[c116])).
% 0.52/0.71 fof(query64,conjecture,(~genls(f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)),c_tptpcol_15_74743)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', query64)).
% 0.52/0.71 fof(c0,negated_conjecture,(~(~genls(f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)),c_tptpcol_15_74743))),inference(assume_negation,[status(cth)],[query64])).
% 0.52/0.71 fof(c1,negated_conjecture,genls(f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)),c_tptpcol_15_74743),inference(fof_simplification,[status(thm)],[c0])).
% 0.52/0.71 cnf(c2,negated_conjecture,genls(f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)),c_tptpcol_15_74743),inference(split_conjunct,[status(thm)],[c1])).
% 0.52/0.71 fof(just10,axiom,(![ARG1]:(![ARG2]:(genls(ARG1,ARG2)=>subsetof(ARG1,ARG2)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just10)).
% 0.52/0.71 fof(c218,plain,(![ARG1]:(![ARG2]:(~genls(ARG1,ARG2)|subsetof(ARG1,ARG2)))),inference(fof_nnf,[status(thm)],[just10])).
% 0.52/0.71 fof(c219,plain,(![X133]:(![X134]:(~genls(X133,X134)|subsetof(X133,X134)))),inference(variable_rename,[status(thm)],[c218])).
% 0.52/0.71 cnf(c220,plain,~genls(X241,X240)|subsetof(X241,X240),inference(split_conjunct,[status(thm)],[c219])).
% 0.52/0.71 cnf(c313,plain,subsetof(f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)),c_tptpcol_15_74743),inference(resolution,[status(thm)],[c220, c2])).
% 0.52/0.71 cnf(c397,plain,setorcollection(f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))),inference(resolution,[status(thm)],[c313, c117])).
% 0.52/0.71 cnf(c400,plain,~individual(f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml))),inference(resolution,[status(thm)],[c397, c236])).
% 0.52/0.71 cnf(c403,plain,$false,inference(resolution,[status(thm)],[c400, c233])).
% 0.52/0.71 % SZS output end CNFRefutation
% 0.52/0.71
% 0.52/0.71 % Initial clauses : 77
% 0.52/0.71 % Processed clauses : 111
% 0.52/0.71 % Factors computed : 4
% 0.52/0.71 % Resolvents computed: 162
% 0.52/0.71 % Tautologies deleted: 25
% 0.52/0.71 % Forward subsumed : 76
% 0.52/0.71 % Backward subsumed : 0
% 0.52/0.71 % -------- CPU Time ---------
% 0.52/0.71 % User time : 0.353 s
% 0.52/0.71 % System time : 0.016 s
% 0.52/0.71 % Total time : 0.369 s
%------------------------------------------------------------------------------