Dave is green. Dave is red. Dave is rough. All nice, rough things are kind. Green, smart things are nice. All green things are quiet. All quiet things are rough. If something is rough and quiet then it is nice. All green, rough things are smart. If something is nice then it is green. Nice, kind things are green.
Dave is green.
("Dave" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
All nice, rough things are kind.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Green, smart things are nice.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
All green things are quiet.
((("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
All quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
If something is rough and quiet then it is nice.
((("something" "is" "rough" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
All green, rough things are smart.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If something is nice then it is green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
Nice, kind things are green.
((("something" "is" "nice" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Dave is red.
True
1
proof
[(triple2)]
("Dave" "is" "red" "+")
triple2
Dave is not red.
False
1
inv-proof
[(triple2)]
("Dave" "is" "red" "-")
triple2
Dave is smart.
True
3
proof
[(((triple1 triple3) -> rule6) OR ((triple1 ((((triple1) -> rule3)) -> rule4)) -> rule6))]
("Dave" "is" "smart" "+")
((triple1 triple3) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is not quiet.
False
2
inv-proof
[(((triple1) -> rule3))]
("Dave" "is" "quiet" "-")
((triple1) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
True
4
proof
[(((triple1 ((triple1 triple3) -> rule6)) -> rule2) OR ((triple3 ((triple1) -> rule3)) -> rule5) OR ((((((triple1) -> rule3)) -> rule4) ((triple1) -> rule3)) -> rule5) OR ((triple1 ((triple1 ((((triple1) -> rule3)) -> rule4)) -> rule6)) -> rule2))]
("Dave" "is" "nice" "+")
((triple1 ((triple1 triple3) -> (rule6 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((triple3 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2)) ((triple1) -> (rule3 % int3))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((triple1 ((triple1 ((((triple1) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is not nice.
False
4
inv-proof
[(((triple1 ((triple1 triple3) -> rule6)) -> rule2) OR ((triple3 ((triple1) -> rule3)) -> rule5) OR ((((((triple1) -> rule3)) -> rule4) ((triple1) -> rule3)) -> rule5) OR ((triple1 ((triple1 ((((triple1) -> rule3)) -> rule4)) -> rule6)) -> rule2))]
("Dave" "is" "nice" "-")
((triple1 ((triple1 triple3) -> (rule6 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((triple3 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2)) ((triple1) -> (rule3 % int3))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((triple1 ((triple1 ((((triple1) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is kind.
True
6
proof
[(((((triple1 ((triple1 triple3) -> rule6)) -> rule2) triple3) -> rule1) OR ((((triple3 ((triple1) -> rule3)) -> rule5) triple3) -> rule1) OR ((((triple1 ((triple1 triple3) -> rule6)) -> rule2) ((((triple1) -> rule3)) -> rule4)) -> rule1) OR ((((triple3 ((triple1) -> rule3)) -> rule5) ((((triple1) -> rule3)) -> rule4)) -> rule1) OR ((((((((triple1) -> rule3)) -> rule4) ((triple1) -> rule3)) -> rule5) triple3) -> rule1) OR ((((((((triple1) -> rule3)) -> rule4) ((triple1) -> rule3)) -> rule5) ((((triple1) -> rule3)) -> rule4)) -> rule1) OR ((((triple1 ((triple1 ((((triple1) -> rule3)) -> rule4)) -> rule6)) -> rule2) triple3) -> rule1) OR ((((triple1 ((triple1 ((((triple1) -> rule3)) -> rule4)) -> rule6)) -> rule2) ((((triple1) -> rule3)) -> rule4)) -> rule1))]
("Dave" "is" "kind" "+")
((((triple1 ((triple1 triple3) -> (rule6 % int3))) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
((((triple3 ((triple1) -> (rule3 % int3))) -> (rule5 % int2)) triple3) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((triple1 ((triple1 triple3) -> (rule6 % int5))) -> (rule2 % int4)) ((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
int5
((((triple3 ((triple1) -> (rule3 % int4))) -> (rule5 % int3)) ((((triple1) -> (rule3 % int4))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
((((((((triple1) -> (rule3 % int4))) -> (rule4 % int3)) ((triple1) -> (rule3 % int4))) -> (rule5 % int2)) triple3) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
((((((((triple1) -> (rule3 % int4))) -> (rule4 % int3)) ((triple1) -> (rule3 % int4))) -> (rule5 % int2)) ((((triple1) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
((((triple1 ((triple1 ((((triple1) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is quiet.
("Dave" "is" "quiet" "+")
int5
((((triple1 ((triple1 ((((triple1) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) ((((triple1) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is quiet.
("Dave" "is" "quiet" "+")
int5
Dave is not kind.
False
6
inv-proof
[(((((triple1 ((triple1 triple3) -> rule6)) -> rule2) triple3) -> rule1) OR ((((triple3 ((triple1) -> rule3)) -> rule5) triple3) -> rule1) OR ((((triple1 ((triple1 triple3) -> rule6)) -> rule2) ((((triple1) -> rule3)) -> rule4)) -> rule1) OR ((((triple3 ((triple1) -> rule3)) -> rule5) ((((triple1) -> rule3)) -> rule4)) -> rule1) OR ((((((((triple1) -> rule3)) -> rule4) ((triple1) -> rule3)) -> rule5) triple3) -> rule1) OR ((((((((triple1) -> rule3)) -> rule4) ((triple1) -> rule3)) -> rule5) ((((triple1) -> rule3)) -> rule4)) -> rule1) OR ((((triple1 ((triple1 ((((triple1) -> rule3)) -> rule4)) -> rule6)) -> rule2) triple3) -> rule1) OR ((((triple1 ((triple1 ((((triple1) -> rule3)) -> rule4)) -> rule6)) -> rule2) ((((triple1) -> rule3)) -> rule4)) -> rule1))]
("Dave" "is" "kind" "-")
((((triple1 ((triple1 triple3) -> (rule6 % int3))) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
((((triple3 ((triple1) -> (rule3 % int3))) -> (rule5 % int2)) triple3) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((triple1 ((triple1 triple3) -> (rule6 % int5))) -> (rule2 % int4)) ((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
int5
((((triple3 ((triple1) -> (rule3 % int4))) -> (rule5 % int3)) ((((triple1) -> (rule3 % int4))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
((((((((triple1) -> (rule3 % int4))) -> (rule4 % int3)) ((triple1) -> (rule3 % int4))) -> (rule5 % int2)) triple3) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
((((((((triple1) -> (rule3 % int4))) -> (rule4 % int3)) ((triple1) -> (rule3 % int4))) -> (rule5 % int2)) ((((triple1) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
((((triple1 ((triple1 ((((triple1) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is quiet.
("Dave" "is" "quiet" "+")
int5
((((triple1 ((triple1 ((((triple1) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) ((((triple1) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is quiet.
("Dave" "is" "quiet" "+")
int5
@0: Dave is green.[(triple1)] Dave is red.[(triple2)] Dave is rough.[(triple3 OR ((((triple1) -> rule3)) -> rule4))] @1: Dave is quiet.[(((triple1) -> rule3))] Dave is smart.[(((triple1 triple3) -> rule6) OR ((triple1 ((((triple1) -> rule3)) -> rule4)) -> rule6))] @2: Dave is nice.[(((triple1 ((triple1 triple3) -> rule6)) -> rule2) OR ((triple3 ((triple1) -> rule3)) -> rule5) OR ((((((triple1) -> rule3)) -> rule4) ((triple1) -> rule3)) -> rule5) OR ((triple1 ((triple1 ((((triple1) -> rule3)) -> rule4)) -> rule6)) -> rule2))] @3: Dave is kind.[(((((triple1 ((triple1 triple3) -> rule6)) -> rule2) triple3) -> rule1) OR ((((triple3 ((triple1) -> rule3)) -> rule5) triple3) -> rule1) OR ((((triple1 ((triple1 triple3) -> rule6)) -> rule2) ((((triple1) -> rule3)) -> rule4)) -> rule1) OR ((((triple3 ((triple1) -> rule3)) -> rule5) ((((triple1) -> rule3)) -> rule4)) -> rule1) OR ((((((((triple1) -> rule3)) -> rule4) ((triple1) -> rule3)) -> rule5) triple3) -> rule1) OR ((((((((triple1) -> rule3)) -> rule4) ((triple1) -> rule3)) -> rule5) ((((triple1) -> rule3)) -> rule4)) -> rule1) OR ((((triple1 ((triple1 ((((triple1) -> rule3)) -> rule4)) -> rule6)) -> rule2) triple3) -> rule1) OR ((((triple1 ((triple1 ((((triple1) -> rule3)) -> rule4)) -> rule6)) -> rule2) ((((triple1) -> rule3)) -> rule4)) -> rule1))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple1 triple3) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
((triple1 ((triple1 triple3) -> (rule6 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((triple3 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2)) ((triple1) -> (rule3 % int3))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((triple1 ((triple1 ((((triple1) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
((((triple1 ((triple1 triple3) -> (rule6 % int3))) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
((((triple3 ((triple1) -> (rule3 % int3))) -> (rule5 % int2)) triple3) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((triple1 ((triple1 triple3) -> (rule6 % int5))) -> (rule2 % int4)) ((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
int5
((((triple3 ((triple1) -> (rule3 % int4))) -> (rule5 % int3)) ((((triple1) -> (rule3 % int4))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
((((((((triple1) -> (rule3 % int4))) -> (rule4 % int3)) ((triple1) -> (rule3 % int4))) -> (rule5 % int2)) triple3) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
((((((((triple1) -> (rule3 % int4))) -> (rule4 % int3)) ((triple1) -> (rule3 % int4))) -> (rule5 % int2)) ((((triple1) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
((((triple1 ((triple1 ((((triple1) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is quiet.
("Dave" "is" "quiet" "+")
int5
((((triple1 ((triple1 ((((triple1) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) ((((triple1) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is quiet.
("Dave" "is" "quiet" "+")
int5