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