Anne is blue. Anne is red. Anne is round. Harry is blue. Harry is green. Harry is quiet. Harry is red. If Harry is big and Harry is blue then Harry is green. All red things are quiet. If Anne is big and Anne is quiet then Anne is nice. All green things are nice. If something is blue then it is green. If something is blue then it is quiet. If something is green and round then it is big. Nice, red things are round.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
If Harry is big and Harry is blue then Harry is green.
((("Harry" "is" "big" "+") ("Harry" "is" "blue" "+")) -> ("Harry" "is" "green" "+"))
All red things are quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
If Anne is big and Anne is quiet then Anne is nice.
((("Anne" "is" "big" "+") ("Anne" "is" "quiet" "+")) -> ("Anne" "is" "nice" "+"))
All green things are nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If something is blue then it is green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If something is blue then it is quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
If something is green and round then it is big.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
Nice, red things are round.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
Anne is round.
True
1
proof
[(triple3 OR ((((((triple1) -> rule5)) -> rule4) triple2) -> rule8))]
("Anne" "is" "round" "+")
triple3
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2)) triple2) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Harry is not red.
False
1
inv-proof
[(triple7)]
("Harry" "is" "red" "-")
triple7
Harry is nice.
True
2
proof
[(((triple5) -> rule4) OR ((((triple4) -> rule5)) -> rule4))]
("Harry" "is" "nice" "+")
((triple5) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Anne is not green.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "green" "-")
((triple1) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
True
4
proof
[(((((triple1) -> rule5) triple3) -> rule7) OR ((((triple1) -> rule5) ((((((triple1) -> rule5)) -> rule4) triple2) -> rule8)) -> rule7))]
("Anne" "is" "big" "+")
((((triple1) -> (rule5 % int2)) triple3) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple1) -> (rule5 % int4)) ((((((triple1) -> (rule5 % int4))) -> (rule4 % int3)) triple2) -> (rule8 % int2))) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is not big.
False
4
inv-proof
[(((((triple1) -> rule5) triple3) -> rule7) OR ((((triple1) -> rule5) ((((((triple1) -> rule5)) -> rule4) triple2) -> rule8)) -> rule7))]
("Anne" "is" "big" "-")
((((triple1) -> (rule5 % int2)) triple3) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple1) -> (rule5 % int4)) ((((((triple1) -> (rule5 % int4))) -> (rule4 % int3)) triple2) -> (rule8 % int2))) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Harry is big.
True
6
proof
[(((triple5 ((((triple5) -> rule4) triple7) -> rule8)) -> rule7) OR ((((triple4) -> rule5) ((((triple5) -> rule4) triple7) -> rule8)) -> rule7) OR ((triple5 ((((((triple4) -> rule5)) -> rule4) triple7) -> rule8)) -> rule7) OR ((((triple4) -> rule5) ((((((triple4) -> rule5)) -> rule4) triple7) -> rule8)) -> rule7))]
("Harry" "is" "big" "+")
((triple5 ((((triple5) -> (rule4 % int3)) triple7) -> (rule8 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple4) -> (rule5 % int4)) ((((triple5) -> (rule4 % int3)) triple7) -> (rule8 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
((triple5 ((((((triple4) -> (rule5 % int4))) -> (rule4 % int3)) triple7) -> (rule8 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
((((triple4) -> (rule5 % int4)) ((((((triple4) -> (rule5 % int4))) -> (rule4 % int3)) triple7) -> (rule8 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is not big.
False
6
inv-proof
[(((triple5 ((((triple5) -> rule4) triple7) -> rule8)) -> rule7) OR ((((triple4) -> rule5) ((((triple5) -> rule4) triple7) -> rule8)) -> rule7) OR ((triple5 ((((((triple4) -> rule5)) -> rule4) triple7) -> rule8)) -> rule7) OR ((((triple4) -> rule5) ((((((triple4) -> rule5)) -> rule4) triple7) -> rule8)) -> rule7))]
("Harry" "is" "big" "-")
((triple5 ((((triple5) -> (rule4 % int3)) triple7) -> (rule8 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple4) -> (rule5 % int4)) ((((triple5) -> (rule4 % int3)) triple7) -> (rule8 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
((triple5 ((((((triple4) -> (rule5 % int4))) -> (rule4 % int3)) triple7) -> (rule8 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
((((triple4) -> (rule5 % int4)) ((((((triple4) -> (rule5 % int4))) -> (rule4 % int3)) triple7) -> (rule8 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
@0: Anne is blue.[(triple1)] Anne is red.[(triple2)] Anne is round.[(triple3 OR ((((((triple1) -> rule5)) -> rule4) triple2) -> rule8))] Harry is blue.[(triple4)] Harry is green.[(triple5 OR ((triple4) -> rule5))] Harry is quiet.[(triple6 OR ((triple4) -> rule6) OR ((triple7) -> rule2))] Harry is red.[(triple7)] @1: Anne is green.[(((triple1) -> rule5))] Anne is quiet.[(((triple1) -> rule6) OR ((triple2) -> rule2))] Harry is nice.[(((triple5) -> rule4) OR ((((triple4) -> rule5)) -> rule4))] @2: Anne is big.[(((((triple1) -> rule5) triple3) -> rule7) OR ((((triple1) -> rule5) ((((((triple1) -> rule5)) -> rule4) triple2) -> rule8)) -> rule7))] Anne is nice.[(((((triple1) -> rule5)) -> rule4) OR ((((((triple1) -> rule5) triple3) -> rule7) ((triple1) -> rule6)) -> rule3) OR ((((((triple1) -> rule5) triple3) -> rule7) ((triple2) -> rule2)) -> rule3))] Harry is round.[(((((triple5) -> rule4) triple7) -> rule8) OR ((((((triple4) -> rule5)) -> rule4) triple7) -> rule8))] @3: Harry is big.[(((triple5 ((((triple5) -> rule4) triple7) -> rule8)) -> rule7) OR ((((triple4) -> rule5) ((((triple5) -> rule4) triple7) -> rule8)) -> rule7) OR ((triple5 ((((((triple4) -> rule5)) -> rule4) triple7) -> rule8)) -> rule7) OR ((((triple4) -> rule5) ((((((triple4) -> rule5)) -> rule4) triple7) -> rule8)) -> rule7))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2)) triple2) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Harry is green.
("Harry" "is" "green" "+")
triple5
((triple4) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple6
((triple4) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple7) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple7
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((triple2) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple5) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule5 % int2)) triple3) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple1) -> (rule5 % int4)) ((((((triple1) -> (rule5 % int4))) -> (rule4 % int3)) triple2) -> (rule8 % int2))) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((((triple1) -> (rule5 % int4)) triple3) -> (rule7 % int3)) ((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
((((((triple1) -> (rule5 % int4)) triple3) -> (rule7 % int3)) ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Harry is round.
("Harry" "is" "round" "+")
((((triple5) -> (rule4 % int2)) triple7) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((((triple4) -> (rule5 % int3))) -> (rule4 % int2)) triple7) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
((triple5 ((((triple5) -> (rule4 % int3)) triple7) -> (rule8 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple4) -> (rule5 % int4)) ((((triple5) -> (rule4 % int3)) triple7) -> (rule8 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
((triple5 ((((((triple4) -> (rule5 % int4))) -> (rule4 % int3)) triple7) -> (rule8 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
((((triple4) -> (rule5 % int4)) ((((((triple4) -> (rule5 % int4))) -> (rule4 % int3)) triple7) -> (rule8 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4