Anne is big. Anne is furry. Anne is white. Charlie is big. Charlie is blue. Charlie is furry. Charlie is nice. Charlie is white. Harry is big. Harry is blue. Harry is furry. Harry is nice. Harry is red. Harry is round. Harry is white. If Charlie is round then Charlie is red. White things are blue. If Anne is white and Anne is nice then Anne is big. If something is blue and round then it is big. If Charlie is furry then Charlie is white. If something is round then it is red. Red, white things are big. White things are round.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If Charlie is round then Charlie is red.
((("Charlie" "is" "round" "+")) -> ("Charlie" "is" "red" "+"))
White things are blue.
((("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
If Anne is white and Anne is nice then Anne is big.
((("Anne" "is" "white" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "big" "+"))
If something is blue and round then it is big.
((("something" "is" "blue" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If Charlie is furry then Charlie is white.
((("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "white" "+"))
If something is round then it is red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
Red, white things are big.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
White things are round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
Harry is red.
True
1
proof
[(triple13 OR ((triple14) -> rule6) OR ((((triple15) -> rule8)) -> rule6))]
("Harry" "is" "red" "+")
triple13
((triple14) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple15) -> (rule8 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Charlie is not blue.
False
1
inv-proof
[(triple5 OR ((triple8) -> rule2) OR ((((triple6) -> rule5)) -> rule2))]
("Charlie" "is" "blue" "-")
triple5
((triple8) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Anne is blue.
True
2
proof
[(((triple3) -> rule2))]
("Anne" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not blue.
False
2
inv-proof
[(((triple3) -> rule2))]
("Anne" "is" "blue" "-")
((triple3) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Charlie is red.
True
3
proof
[(((((triple8) -> rule8)) -> rule1) OR ((((triple8) -> rule8)) -> rule6) OR ((((((triple6) -> rule5)) -> rule8)) -> rule1) OR ((((((triple6) -> rule5)) -> rule8)) -> rule6))]
("Charlie" "is" "red" "+")
((((triple8) -> (rule8 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((triple8) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((((triple6) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((((triple6) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is not red.
False
3
inv-proof
[(((((triple8) -> rule8)) -> rule1) OR ((((triple8) -> rule8)) -> rule6) OR ((((((triple6) -> rule5)) -> rule8)) -> rule1) OR ((((((triple6) -> rule5)) -> rule8)) -> rule6))]
("Charlie" "is" "red" "-")
((((triple8) -> (rule8 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((triple8) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((((triple6) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((((triple6) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
@0: Anne is big.[(triple1 OR ((((triple3) -> rule2) ((triple3) -> rule8)) -> rule4) OR ((((((triple3) -> rule8)) -> rule6) triple3) -> rule7))] Anne is furry.[(triple2)] Anne is white.[(triple3)] Charlie is big.[(triple4 OR ((triple5 ((triple8) -> rule8)) -> rule4) OR ((((triple8) -> rule2) ((triple8) -> rule8)) -> rule4) OR ((triple5 ((((triple6) -> rule5)) -> rule8)) -> rule4) OR ((((((triple8) -> rule8)) -> rule1) triple8) -> rule7) OR ((((((triple8) -> rule8)) -> rule6) triple8) -> rule7) OR ((((triple8) -> rule2) ((((triple6) -> rule5)) -> rule8)) -> rule4) OR ((((((triple6) -> rule5)) -> rule2) ((triple8) -> rule8)) -> rule4) OR ((((((triple8) -> rule8)) -> rule1) ((triple6) -> rule5)) -> rule7) OR ((((((triple8) -> rule8)) -> rule6) ((triple6) -> rule5)) -> rule7) OR ((((((triple6) -> rule5)) -> rule2) ((((triple6) -> rule5)) -> rule8)) -> rule4) OR ((((((((triple6) -> rule5)) -> rule8)) -> rule1) triple8) -> rule7) OR ((((((((triple6) -> rule5)) -> rule8)) -> rule6) triple8) -> rule7) OR ((((((((triple6) -> rule5)) -> rule8)) -> rule1) ((triple6) -> rule5)) -> rule7) OR ((((((((triple6) -> rule5)) -> rule8)) -> rule6) ((triple6) -> rule5)) -> rule7))] Charlie is blue.[(triple5 OR ((triple8) -> rule2) OR ((((triple6) -> rule5)) -> rule2))] Charlie is furry.[(triple6)] Charlie is nice.[(triple7)] Charlie is white.[(triple8 OR ((triple6) -> rule5))] Harry is big.[(triple9 OR ((triple10 triple14) -> rule4) OR ((triple13 triple15) -> rule7) OR ((triple10 ((triple15) -> rule8)) -> rule4) OR ((((triple14) -> rule6) triple15) -> rule7) OR ((((triple15) -> rule2) triple14) -> rule4) OR ((((triple15) -> rule2) ((triple15) -> rule8)) -> rule4) OR ((((((triple15) -> rule8)) -> rule6) triple15) -> rule7))] Harry is blue.[(triple10 OR ((triple15) -> rule2))] Harry is furry.[(triple11)] Harry is nice.[(triple12)] Harry is red.[(triple13 OR ((triple14) -> rule6) OR ((((triple15) -> rule8)) -> rule6))] Harry is round.[(triple14 OR ((triple15) -> rule8))] Harry is white.[(triple15)] @1: Anne is blue.[(((triple3) -> rule2))] Anne is round.[(((triple3) -> rule8))] Charlie is round.[(((triple8) -> rule8) OR ((((triple6) -> rule5)) -> rule8))] @2: Anne is red.[(((((triple3) -> rule8)) -> rule6))] Charlie is red.[(((((triple8) -> rule8)) -> rule1) OR ((((triple8) -> rule8)) -> rule6) OR ((((((triple6) -> rule5)) -> rule8)) -> rule1) OR ((((((triple6) -> rule5)) -> rule8)) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((((triple3) -> (rule2 % int3)) ((triple3) -> (rule8 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((((((triple3) -> (rule8 % int3))) -> (rule6 % int2)) triple3) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
triple4
((triple5 ((triple8) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((triple8) -> (rule2 % int3)) ((triple8) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
((triple5 ((((triple6) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((((triple8) -> (rule8 % int3))) -> (rule1 % int2)) triple8) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
((((((triple8) -> (rule8 % int3))) -> (rule6 % int2)) triple8) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
((((triple8) -> (rule2 % int4)) ((((triple6) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
((((((triple6) -> (rule5 % int4))) -> (rule2 % int3)) ((triple8) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
((((((triple8) -> (rule8 % int4))) -> (rule1 % int3)) ((triple6) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
((((((triple8) -> (rule8 % int4))) -> (rule6 % int3)) ((triple6) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
((((((triple6) -> (rule5 % int4))) -> (rule2 % int3)) ((((triple6) -> (rule5 % int4))) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
((((((((triple6) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule1 % int2)) triple8) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
((((((((triple6) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule6 % int2)) triple8) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
((((((((triple6) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule1 % int2)) ((triple6) -> (rule5 % int4))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
((((((((triple6) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule6 % int2)) ((triple6) -> (rule5 % int4))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
((triple8) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple6
Charlie is nice.
("Charlie" "is" "nice" "+")
triple7
Charlie is white.
("Charlie" "is" "white" "+")
triple8
((triple6) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple9
((triple10 triple14) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple13 triple15) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple10 ((triple15) -> (rule8 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((((triple14) -> (rule6 % int2)) triple15) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple15) -> (rule2 % int2)) triple14) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple15) -> (rule2 % int3)) ((triple15) -> (rule8 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((triple15) -> (rule8 % int3))) -> (rule6 % int2)) triple15) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
triple10
((triple15) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple11
Harry is nice.
("Harry" "is" "nice" "+")
triple12
Harry is red.
("Harry" "is" "red" "+")
triple13
((triple14) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple15) -> (rule8 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
triple14
((triple15) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple15
Anne is blue.
("Anne" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple3) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple8) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((((triple3) -> (rule8 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((((triple8) -> (rule8 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((triple8) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((((triple6) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((((triple6) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3