Anne is big. Anne is blue. Anne is nice. Anne is quiet. Anne is red. Anne is rough. Anne is white. Harry is big. Harry is blue. Harry is nice. Harry is quiet. Harry is white. If Anne is blue then Anne is quiet. White people are quiet. If Anne is rough and Anne is big then Anne is white. All blue, white people are red. Big, white people are blue. Red people are white.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is white.
("Anne" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is white.
("Harry" "is" "white" "+")
If Anne is blue then Anne is quiet.
((("Anne" "is" "blue" "+")) -> ("Anne" "is" "quiet" "+"))
White people are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If Anne is rough and Anne is big then Anne is white.
((("Anne" "is" "rough" "+") ("Anne" "is" "big" "+")) -> ("Anne" "is" "white" "+"))
All blue, white people are red.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
Big, white people are blue.
((("someone" "is" "big" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
Red people are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
Harry is quiet.
True
1
proof
[(triple11 OR ((triple12) -> rule2))]
("Harry" "is" "quiet" "+")
triple11
((triple12) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Anne is not blue.
False
1
inv-proof
[(triple2 OR ((triple1 triple7) -> rule5) OR ((triple1 ((triple5) -> rule6)) -> rule5) OR ((triple1 ((triple6 triple1) -> rule3)) -> rule5))]
("Anne" "is" "blue" "-")
triple2
((triple1 triple7) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple1 ((triple5) -> (rule6 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((triple1 ((triple6 triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
@0: Anne is big.[(triple1)] Anne is blue.[(triple2 OR ((triple1 triple7) -> rule5) OR ((triple1 ((triple5) -> rule6)) -> rule5) OR ((triple1 ((triple6 triple1) -> rule3)) -> rule5))] Anne is nice.[(triple3)] Anne is quiet.[(triple4 OR ((triple2) -> rule1) OR ((triple7) -> rule2) OR ((((triple5) -> rule6)) -> rule2) OR ((((triple1 triple7) -> rule5)) -> rule1) OR ((((triple6 triple1) -> rule3)) -> rule2) OR ((((triple1 ((triple5) -> rule6)) -> rule5)) -> rule1) OR ((((triple1 ((triple6 triple1) -> rule3)) -> rule5)) -> rule1))] Anne is red.[(triple5 OR ((triple2 triple7) -> rule4) OR ((triple2 ((triple6 triple1) -> rule3)) -> rule4) OR ((((triple1 triple7) -> rule5) triple7) -> rule4) OR ((((triple1 triple7) -> rule5) ((triple6 triple1) -> rule3)) -> rule4) OR ((((triple1 ((triple6 triple1) -> rule3)) -> rule5) triple7) -> rule4) OR ((((triple1 ((triple6 triple1) -> rule3)) -> rule5) ((triple6 triple1) -> rule3)) -> rule4))] Anne is rough.[(triple6)] Anne is white.[(triple7 OR ((triple5) -> rule6) OR ((triple6 triple1) -> rule3))] Harry is big.[(triple8)] Harry is blue.[(triple9 OR ((triple8 triple12) -> rule5))] Harry is nice.[(triple10)] Harry is quiet.[(triple11 OR ((triple12) -> rule2))] Harry is white.[(triple12)] @1: Harry is red.[(((triple9 triple12) -> rule4) OR ((((triple8 triple12) -> rule5) triple12) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
((triple1 triple7) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple1 ((triple5) -> (rule6 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((triple1 ((triple6 triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
((triple2) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((triple7) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple5) -> (rule6 % int2))) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((triple1 triple7) -> (rule5 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((triple6 triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((triple1 ((triple5) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((((triple1 ((triple6 triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
triple5
((triple2 triple7) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple2 ((triple6 triple1) -> (rule3 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((triple1 triple7) -> (rule5 % int2)) triple7) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((triple1 triple7) -> (rule5 % int3)) ((triple6 triple1) -> (rule3 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((((triple1 ((triple6 triple1) -> (rule3 % int3))) -> (rule5 % int2)) triple7) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((((triple1 ((triple6 triple1) -> (rule3 % int3))) -> (rule5 % int2)) ((triple6 triple1) -> (rule3 % int3))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
triple6
Anne is white.
("Anne" "is" "white" "+")
triple7
((triple5) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple6 triple1) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
((triple8 triple12) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
((triple12) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple12
Harry is red.
("Harry" "is" "red" "+")
((triple9 triple12) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple8 triple12) -> (rule5 % int2)) triple12) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2