Anne is big. Anne is green. Anne is nice. Anne is quiet. Anne is red. Charlie is big. Charlie is green. Charlie is nice. Charlie is quiet. Charlie is red. Charlie is rough. Dave is big. Dave is nice. Dave is quiet. Dave is red. Dave is rough. If Anne is kind and Anne is rough then Anne is red. Big, nice things are quiet. If Anne is nice then Anne is rough. Quiet, rough things are kind. Kind things are green. All rough, big things are red.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
If Anne is kind and Anne is rough then Anne is red.
((("Anne" "is" "kind" "+") ("Anne" "is" "rough" "+")) -> ("Anne" "is" "red" "+"))
Big, nice things are quiet.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
If Anne is nice then Anne is rough.
((("Anne" "is" "nice" "+")) -> ("Anne" "is" "rough" "+"))
Quiet, rough things are kind.
((("something" "is" "quiet" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
All rough, big things are red.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
Dave is rough.
True
1
proof
[(triple16)]
("Dave" "is" "rough" "+")
triple16
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Dave is kind.
True
3
proof
[(((triple14 triple16) -> rule4) OR ((((triple12 triple13) -> rule2) triple16) -> rule4))]
("Dave" "is" "kind" "+")
((triple14 triple16) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple12 triple13) -> (rule2 % int2)) triple16) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not kind.
False
3
inv-proof
[(((triple14 triple16) -> rule4) OR ((((triple12 triple13) -> rule2) triple16) -> rule4))]
("Dave" "is" "kind" "-")
((triple14 triple16) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple12 triple13) -> (rule2 % int2)) triple16) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
@0: Anne is big.[(triple1)] Anne is green.[(triple2 OR ((((triple4 ((triple3) -> rule3)) -> rule4)) -> rule5) OR ((((((triple1 triple3) -> rule2) ((triple3) -> rule3)) -> rule4)) -> rule5))] Anne is nice.[(triple3)] Anne is quiet.[(triple4 OR ((triple1 triple3) -> rule2))] Anne is red.[(triple5 OR ((((triple3) -> rule3) triple1) -> rule6) OR ((((triple4 ((triple3) -> rule3)) -> rule4) ((triple3) -> rule3)) -> rule1) OR ((((((triple1 triple3) -> rule2) ((triple3) -> rule3)) -> rule4) ((triple3) -> rule3)) -> rule1))] Charlie is big.[(triple6)] Charlie is green.[(triple7 OR ((((triple9 triple11) -> rule4)) -> rule5) OR ((((((triple6 triple8) -> rule2) triple11) -> rule4)) -> rule5))] Charlie is nice.[(triple8)] Charlie is quiet.[(triple9 OR ((triple6 triple8) -> rule2))] Charlie is red.[(triple10 OR ((triple11 triple6) -> rule6))] Charlie is rough.[(triple11)] Dave is big.[(triple12)] Dave is nice.[(triple13)] Dave is quiet.[(triple14 OR ((triple12 triple13) -> rule2))] Dave is red.[(triple15 OR ((triple16 triple12) -> rule6))] Dave is rough.[(triple16)] @1: Anne is rough.[(((triple3) -> rule3))] Charlie is kind.[(((triple9 triple11) -> rule4) OR ((((triple6 triple8) -> rule2) triple11) -> rule4))] Dave is kind.[(((triple14 triple16) -> rule4) OR ((((triple12 triple13) -> rule2) triple16) -> rule4))] @2: Anne is kind.[(((triple4 ((triple3) -> rule3)) -> rule4) OR ((((triple1 triple3) -> rule2) ((triple3) -> rule3)) -> rule4))] Dave is green.[(((((triple14 triple16) -> rule4)) -> rule5) OR ((((((triple12 triple13) -> rule2) triple16) -> rule4)) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((((triple4 ((triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
((((((triple1 triple3) -> (rule2 % int4)) ((triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
((triple1 triple3) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple5
((((triple3) -> (rule3 % int2)) triple1) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((triple4 ((triple3) -> (rule3 % int3))) -> (rule4 % int2)) ((triple3) -> (rule3 % int3))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
((((((triple1 triple3) -> (rule2 % int4)) ((triple3) -> (rule3 % int3))) -> (rule4 % int2)) ((triple3) -> (rule3 % int3))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Charlie is big.
("Charlie" "is" "big" "+")
triple6
Charlie is green.
("Charlie" "is" "green" "+")
triple7
((((triple9 triple11) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((((triple6 triple8) -> (rule2 % int3)) triple11) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple8
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple9
((triple6 triple8) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple10
((triple11 triple6) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple11
Dave is big.
("Dave" "is" "big" "+")
triple12
Dave is nice.
("Dave" "is" "nice" "+")
triple13
Dave is quiet.
("Dave" "is" "quiet" "+")
triple14
((triple12 triple13) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple15
((triple16 triple12) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple16
Anne is rough.
("Anne" "is" "rough" "+")
((triple3) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple9 triple11) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple6 triple8) -> (rule2 % int2)) triple11) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((triple14 triple16) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple12 triple13) -> (rule2 % int2)) triple16) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((triple4 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((triple1 triple3) -> (rule2 % int3)) ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
((((triple14 triple16) -> (rule4 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((((triple12 triple13) -> (rule2 % int3)) triple16) -> (rule4 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3