Simple output format unavailable for versions 0.7 and 0.8 ; description errors

[xamidi]

According to the description

-tptp
   if present, use tptp output format, otherwise a simple output format
-json
   if present, use json output format, otherwise a simple output format

the simple output format should be default, but -tptp is the actual default for versions 0.7 and 0.8.

Moreover,

-print <nr>
   indicate the amount of output: 10 is default, bigger numbers give more,
   useful values are 1,10,11,12,13,14,20,30,40,50,51

but the default seems higher (13 or 14) for versions 0.7 and 0.8.

For example, with -print 10 on GKC 0.8:

result: proof found
for gkc-in.txt 
% SZS status Unsatisfiable for gkc-in.txt 

% SZS output start CNFRefutation for gkc-in.txt 
cnf('1', plain, (t(i(i(i(i(i(X,Y),i(n(Z),n(U))),Z),V),i(i(V,X),i(U,X))))),
  inference(cnf_transformation,[],['m'])).
cnf('2', plain, (~t(i(X,Y)) | ~t(X) | t(Y)),
  inference(cnf_transformation,[],['mp'])).
cnf('3', plain, (~t(i(i(i(i(i(i(X,Y),i(n(Z),n(U))),Z),V),i(i(V,X),i(U,X))),W)) | t(W)),
  inference(resolution,[],['1','2'])).
cnf('4', plain, (t(i(i(i(i(X,Y),i(Z,Y)),i(Y,U)),i(V,i(Y,U))))),
  inference(resolution,[],['3','1'])).
cnf('5', plain, (~t(i(i(i(i(i(X,Y),i(Z,Y)),i(Y,U)),i(V,i(Y,U))),W)) | t(W)),
  inference(resolution,[],['4','2'])).
cnf('6', plain, (t(i(i(i(X,i(n(Y),Z)),U),i(Y,U)))),
  inference(resolution,[],['5','1'])).
cnf('7', plain, (~t(i(i(i(i(X,i(n(Y),Z)),U),i(Y,U)),V)) | t(V)),
  inference(resolution,[],['6','2'])).
cnf('8', plain, (t(i(i(i(X,X),Y),i(Z,Y)))),
  inference(resolution,[],['7','1'])).
cnf('9', plain, (~t(i(i(i(i(X,X),Y),i(Z,Y)),U)) | t(U)),
  inference(resolution,[],['8','2'])).
cnf('10', plain, (t(i(X,i(Y,i(Z,Y))))),
  inference(resolution,[],['9','4'])).
cnf('11', plain, (~t(i(i(X,i(Y,i(Z,Y))),U)) | t(U)),
  inference(resolution,[],['10','2'])).
cnf('12', plain, (t(i(X,i(Y,X)))),
  inference(resolution,[],['11','10'])).
cnf('13', plain, (~t(i(a,i(b,a)))),
  inference(cnf_transformation,[],['a1'])).
cnf('14', plain, ($false),
  inference(resolution,[],['12','13'])).

% SZS output end CNFRefutation for gkc-in.txt 

Without -print <nr> on GKC 0.8:

**** run 1 fork 0 starts with strategy

**** run 2 fork 1 starts with strategy

**** run 3 fork 2 starts with strategy

**** run 4 fork 3 starts with strategy

**** run 5 fork 4 starts with strategy

**** run 6 fork 5 starts with strategy

**** run 7 fork 6 starts with strategy

**** run 8 fork 7 starts with strategy


result: proof found
for gkc-in.txt 
% SZS status Unsatisfiable for gkc-in.txt 

% SZS output start CNFRefutation for gkc-in.txt 
cnf('1', plain, (t(i(i(i(i(i(X,Y),i(n(Z),n(U))),Z),V),i(i(V,X),i(U,X))))),
  inference(cnf_transformation,[],['m'])).
cnf('2', plain, (~t(i(X,Y)) | ~t(X) | t(Y)),
  inference(cnf_transformation,[],['mp'])).
cnf('3', plain, (~t(i(i(i(i(i(i(X,Y),i(n(Z),n(U))),Z),V),i(i(V,X),i(U,X))),W)) | t(W)),
  inference(resolution,[],['1','2'])).
cnf('4', plain, (t(i(i(i(i(X,Y),i(Z,Y)),i(Y,U)),i(V,i(Y,U))))),
  inference(resolution,[],['3','1'])).
cnf('5', plain, (~t(i(i(i(i(i(X,Y),i(Z,Y)),i(Y,U)),i(V,i(Y,U))),W)) | t(W)),
  inference(resolution,[],['4','2'])).
cnf('6', plain, (t(i(i(i(X,i(n(Y),Z)),U),i(Y,U)))),
  inference(resolution,[],['5','1'])).
cnf('7', plain, (~t(i(i(i(i(X,i(n(Y),Z)),U),i(Y,U)),V)) | t(V)),
  inference(resolution,[],['6','2'])).
cnf('8', plain, (t(i(i(i(X,X),Y),i(Z,Y)))),
  inference(resolution,[],['7','1'])).
cnf('9', plain, (~t(i(i(i(i(X,X),Y),i(Z,Y)),U)) | t(U)),
  inference(resolution,[],['8','2'])).
cnf('10', plain, (t(i(X,i(Y,i(Z,Y))))),
  inference(resolution,[],['9','4'])).
cnf('11', plain, (~t(i(i(X,i(Y,i(Z,Y))),U)) | t(U)),
  inference(resolution,[],['10','2'])).
cnf('12', plain, (t(i(X,i(Y,X)))),
  inference(resolution,[],['11','10'])).
cnf('13', plain, (~t(i(a,i(b,a)))),
  inference(cnf_transformation,[],['a1'])).
cnf('14', plain, ($false),
  inference(resolution,[],['12','13'])).

% SZS output end CNFRefutation for gkc-in.txt 

run 7 fork 6 statistics:
----------------------------------
this run seconds: 0.001027
total seconds: 0.002498
stat_given_used: 14
stat_given_used_at_endgame: 0
stat_given_candidates:   38
stat_given_candidates_at_endgame: 0
stat_given_candidates_h: 21
stat_binres_derived_cl:   142
stat_binres_derived_cl_h: 23
stat_factor_derived_cl: 0
stat_para_derived_cl: 0
stat_tautologies_discarded: 1
stat_forward_subsumed: 69
stat_derived_cut: 0
stat_derived_rewritten: 0
stat_weight_discarded_building: 0
stat_weight_discarded_cl: 0
stat_internlimit_discarded_cl: 0
stat_simplified:  0 simplified 0 derived 0 given
stat_kept_cl: 48
stat_built_cl: 141
stat_hyperres_partial_cl: 23
stat_made_rewriters: 0
stat_backward_subsumed: 0
stat_propagated_subsumed: 0
stat_clsubs_attempted:                        45
stat_clsubs_fact_groundunit_found:             0
stat_clsubs_rule_groundunit_found:             1
stat_clsubs_top_meta_attempted:                232
stat_clsubs_top_meta_failed:                   187
stat_clsubs_top_meta_nonpref_attempted:                 232
stat_clsubs_top_meta_nonpref_succeeded:                  45
stat_clsubs_top_meta_pref_attempted:                     45
stat_clsubs_top_meta_pref1_succeeded:                    45
stat_clsubs_top_meta_pref2_succeeded:                    45
stat_clsubs_top_meta_pref3_succeeded:                    45
stat_clsubs_top_meta_pref_succeeded:                     45
stat_clsubs_meta_attempted:                   47
stat_clsubs_meta_failed:                      35
stat_clsubs_predsymbs_attempted:               0
stat_clsubs_unit_attempted:                   44
stat_clsubs_full_attempted:                    1
stat_forwardsubs_attempted:                  140
stat_lit_hash_added:                     51
stat_lit_hash_computed:                 373
stat_lit_hash_match_found:               70
stat_lit_hash_match_miss:               394
stat_lit_hash_cut_ok:                     0
stat_lit_strong_cut_ok:                   0
stat_lit_hash_subsume_ok:                69
clqueue els 10000000 used 1
clactive els 10000000 used 15
clactivesubsume els 10000000 used 79
queue_termbuf els 200000000 used 3277
hyper_termbuf els 100000000 used 1448
active_termbuf els 100000000 used 1699
varstack els 5000 last used 1
given_termbuf els 10000000 last used 1
simplified_termbuf els 10000000 last used 1
derived_termbuf els 10000000 last used 5
wr_mallocs: 170
wr_callocs: 19
wr_reallocs: 1
wr_frees: 2
wr_malloc_bytes: 4162584644
wr_calloc_bytes: 96065504
wr_realloc_bytes: 2000
wr_realloc_freebytes: 0
----------------------------------

Note that also

-parallel <nr of parallel processes to run>
   UNIX only; if omitted, 4 worker processes and 1 parent used

is not fulfilled since 8 processes were used by default.

This works correctly for GKC 0.6, which also generates the expected output:

result: proof found
for gkc-in.txt 

proof:
 1: [in,m] t(i(i(i(i(i(X,Y),i(n(Z),n(U))),Z),V),i(i(V,X),i(U,X)))).
 2: [in,mp] -t(i(X,Y)) | -t(X) | t(Y).
 3: [mp, 1, 2.1] -t(i(i(i(i(i(i(X,Y),i(n(Z),n(U))),Z),V),i(i(V,X),i(U,X))),W)) | t(W).
 4: [mp, 3, 1] t(i(i(i(i(X,Y),i(Z,Y)),i(Y,U)),i(V,i(Y,U)))).
 5: [mp, 4, 2.1] -t(i(i(i(i(i(X,Y),i(Z,Y)),i(Y,U)),i(V,i(Y,U))),W)) | t(W).
 6: [mp, 5, 1] t(i(i(i(X,i(n(Y),Z)),U),i(Y,U))).
 7: [mp, 6, 2.1] -t(i(i(i(i(X,i(n(Y),Z)),U),i(Y,U)),V)) | t(V).
 8: [mp, 7, 1] t(i(i(i(X,X),Y),i(Z,Y))).
 9: [mp, 8, 2.1] -t(i(i(i(i(X,X),Y),i(Z,Y)),U)) | t(U).
 10: [mp, 9, 4] t(i(X,i(Y,i(Z,Y)))).
 11: [mp, 10, 2.1] -t(i(i(X,i(Y,i(Z,Y))),U)) | t(U).
 12: [mp, 11, 10] t(i(X,i(Y,X))).
 13: [in,a1] -t(i(a,i(b,a))).
 14: [mp, 12, 13] false

Tested on Rocky Linux 8.8.

Is there is an undocumented way to use the simple output format with GKC 0.8?

[tammet]

You are right: the simple format works only for GKC 0.6, but not 0.7 or 0.8. Thx for pointing this out! Will put the simple format option back for the next version. A note about 0.7 and 0.8 though: these versions are optimized for the CASC competition and are just slightly better than 0.6. For normal use the version 0.6 is perfectly OK.

[DustinWehr]

FYI gkc -convert -json file.p isn't working either.

{"error": "do not set both -tptp and -json output parameters at the same time"}

I will switch to 0.6. Thanks!