Anne is green. Anne is red. Anne is round. Anne is white. Bob is red. Bob is rough. Bob is young. Gary is blue. Gary is red. Gary is round. Gary is white. Gary is young. Harry is green. Harry is red. Harry is rough. Harry is young. All white, red things are rough. If something is green and white then it is rough. Green things are blue. All green, red things are white. All blue, rough things are round. If Bob is rough then Bob is blue. Blue, round things are green. If something is rough then it is young.
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is young.
("Harry" "is" "young" "+")
All white, red things are rough.
((("something" "is" "white" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If something is green and white then it is rough.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
Green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
All green, red things are white.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
All blue, rough things are round.
((("something" "is" "blue" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If Bob is rough then Bob is blue.
((("Bob" "is" "rough" "+")) -> ("Bob" "is" "blue" "+"))
Blue, round things are green.
((("something" "is" "blue" "+") ("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If something is rough then it is young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
Anne is white.
True
1
proof
[(triple4 OR ((triple1 triple2) -> rule4))]
("Anne" "is" "white" "+")
triple4
((triple1 triple2) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not green.
False
1
inv-proof
[(triple1)]
("Anne" "is" "green" "-")
triple1
Gary is green.
True
3
proof
[(((triple8 triple10) -> rule7) OR ((triple8 ((triple8 ((triple11 triple9) -> rule1)) -> rule5)) -> rule7))]
("Gary" "is" "green" "+")
((triple8 triple10) -> (rule7 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple8 ((triple8 ((triple11 triple9) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Anne is not rough.
False
3
inv-proof
[(((triple1 triple4) -> rule2) OR ((triple4 triple2) -> rule1) OR ((triple1 ((triple1 triple2) -> rule4)) -> rule2) OR ((((triple1 triple2) -> rule4) triple2) -> rule1))]
("Anne" "is" "rough" "-")
((triple1 triple4) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple4 triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple1 ((triple1 triple2) -> (rule4 % int2))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((triple1 triple2) -> (rule4 % int2)) triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Harry is round.
True
4
proof
[(((((triple13) -> rule3) triple15) -> rule5) OR ((((triple13) -> rule3) ((triple13 ((triple13 triple14) -> rule4)) -> rule2)) -> rule5) OR ((((triple13) -> rule3) ((((triple13 triple14) -> rule4) triple14) -> rule1)) -> rule5))]
("Harry" "is" "round" "+")
((((triple13) -> (rule3 % int2)) triple15) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple13) -> (rule3 % int4)) ((triple13 ((triple13 triple14) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
((((triple13) -> (rule3 % int4)) ((((triple13 triple14) -> (rule4 % int3)) triple14) -> (rule1 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is not round.
False
4
inv-proof
[(((((triple13) -> rule3) triple15) -> rule5) OR ((((triple13) -> rule3) ((triple13 ((triple13 triple14) -> rule4)) -> rule2)) -> rule5) OR ((((triple13) -> rule3) ((((triple13 triple14) -> rule4) triple14) -> rule1)) -> rule5))]
("Harry" "is" "round" "-")
((((triple13) -> (rule3 % int2)) triple15) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple13) -> (rule3 % int4)) ((triple13 ((triple13 triple14) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
((((triple13) -> (rule3 % int4)) ((((triple13 triple14) -> (rule4 % int3)) triple14) -> (rule1 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Bob is green.
True
7
proof
[(((((triple6) -> rule6) ((((triple6) -> rule6) triple6) -> rule5)) -> rule7))]
("Bob" "is" "green" "+")
((((triple6) -> (rule6 % int3)) ((((triple6) -> (rule6 % int3)) triple6) -> (rule5 % int2))) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is not green.
False
7
inv-proof
[(((((triple6) -> rule6) ((((triple6) -> rule6) triple6) -> rule5)) -> rule7))]
("Bob" "is" "green" "-")
((((triple6) -> (rule6 % int3)) ((((triple6) -> (rule6 % int3)) triple6) -> (rule5 % int2))) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
@0: Anne is green.[(triple1)] Anne is red.[(triple2)] Anne is round.[(triple3 OR ((((triple1) -> rule3) ((triple1 triple4) -> rule2)) -> rule5) OR ((((triple1) -> rule3) ((triple4 triple2) -> rule1)) -> rule5) OR ((((triple1) -> rule3) ((triple1 ((triple1 triple2) -> rule4)) -> rule2)) -> rule5) OR ((((triple1) -> rule3) ((((triple1 triple2) -> rule4) triple2) -> rule1)) -> rule5))] Anne is white.[(triple4 OR ((triple1 triple2) -> rule4))] Bob is red.[(triple5)] Bob is rough.[(triple6)] Bob is young.[(triple7 OR ((triple6) -> rule8))] Gary is blue.[(triple8)] Gary is red.[(triple9)] Gary is round.[(triple10 OR ((triple8 ((triple11 triple9) -> rule1)) -> rule5))] Gary is white.[(triple11 OR ((((triple8 triple10) -> rule7) triple9) -> rule4))] Gary is young.[(triple12 OR ((((triple11 triple9) -> rule1)) -> rule8) OR ((((((triple8 triple10) -> rule7) triple11) -> rule2)) -> rule8) OR ((((((((triple8 triple10) -> rule7) triple9) -> rule4) triple9) -> rule1)) -> rule8) OR ((((((triple8 triple10) -> rule7) ((((triple8 triple10) -> rule7) triple9) -> rule4)) -> rule2)) -> rule8))] Harry is green.[(triple13)] Harry is red.[(triple14)] Harry is rough.[(triple15 OR ((triple13 ((triple13 triple14) -> rule4)) -> rule2) OR ((((triple13 triple14) -> rule4) triple14) -> rule1))] Harry is young.[(triple16 OR ((triple15) -> rule8) OR ((((triple13 ((triple13 triple14) -> rule4)) -> rule2)) -> rule8) OR ((((((triple13 triple14) -> rule4) triple14) -> rule1)) -> rule8))] @1: Anne is blue.[(((triple1) -> rule3))] Anne is rough.[(((triple1 triple4) -> rule2) OR ((triple4 triple2) -> rule1) OR ((triple1 ((triple1 triple2) -> rule4)) -> rule2) OR ((((triple1 triple2) -> rule4) triple2) -> rule1))] Bob is blue.[(((triple6) -> rule6))] Gary is green.[(((triple8 triple10) -> rule7) OR ((triple8 ((triple8 ((triple11 triple9) -> rule1)) -> rule5)) -> rule7))] Gary is rough.[(((triple11 triple9) -> rule1) OR ((((triple8 triple10) -> rule7) triple11) -> rule2) OR ((((((triple8 triple10) -> rule7) triple9) -> rule4) triple9) -> rule1) OR ((((triple8 triple10) -> rule7) ((((triple8 triple10) -> rule7) triple9) -> rule4)) -> rule2))] Harry is blue.[(((triple13) -> rule3))] Harry is white.[(((triple13 triple14) -> rule4))] @2: Anne is young.[(((((triple1 triple4) -> rule2)) -> rule8) OR ((((triple4 triple2) -> rule1)) -> rule8) OR ((((triple1 ((triple1 triple2) -> rule4)) -> rule2)) -> rule8) OR ((((((triple1 triple2) -> rule4) triple2) -> rule1)) -> rule8))] Bob is round.[(((((triple6) -> rule6) triple6) -> rule5))] Harry is round.[(((((triple13) -> rule3) triple15) -> rule5) OR ((((triple13) -> rule3) ((triple13 ((triple13 triple14) -> rule4)) -> rule2)) -> rule5) OR ((((triple13) -> rule3) ((((triple13 triple14) -> rule4) triple14) -> rule1)) -> rule5))] @3: Bob is green.[(((((triple6) -> rule6) ((((triple6) -> rule6) triple6) -> rule5)) -> rule7))] @4: Bob is white.[(((((((triple6) -> rule6) ((((triple6) -> rule6) triple6) -> rule5)) -> rule7) triple5) -> rule4))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
((((triple1) -> (rule3 % int3)) ((triple1 triple4) -> (rule2 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((((triple1) -> (rule3 % int3)) ((triple4 triple2) -> (rule1 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((((triple1) -> (rule3 % int4)) ((triple1 ((triple1 triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
((((triple1) -> (rule3 % int4)) ((((triple1 triple2) -> (rule4 % int3)) triple2) -> (rule1 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
triple4
((triple1 triple2) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is rough.
("Bob" "is" "rough" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple6) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple8
Gary is red.
("Gary" "is" "red" "+")
triple9
Gary is round.
("Gary" "is" "round" "+")
triple10
((triple8 ((triple11 triple9) -> (rule1 % int2))) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
triple11
((((triple8 triple10) -> (rule7 % int2)) triple9) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
triple12
((((triple11 triple9) -> (rule1 % int2))) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((((triple8 triple10) -> (rule7 % int3)) triple11) -> (rule2 % int2))) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((((((((triple8 triple10) -> (rule7 % int4)) triple9) -> (rule4 % int3)) triple9) -> (rule1 % int2))) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
((((((triple8 triple10) -> (rule7 % int4)) ((((triple8 triple10) -> (rule7 % int4)) triple9) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Harry is green.
("Harry" "is" "green" "+")
triple13
Harry is red.
("Harry" "is" "red" "+")
triple14
Harry is rough.
("Harry" "is" "rough" "+")
triple15
((triple13 ((triple13 triple14) -> (rule4 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple13 triple14) -> (rule4 % int2)) triple14) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
triple16
((triple15) -> (rule8 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple13 ((triple13 triple14) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((((triple13 triple14) -> (rule4 % int3)) triple14) -> (rule1 % int2))) -> (rule8 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((triple1 triple4) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple4 triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple1 ((triple1 triple2) -> (rule4 % int2))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((triple1 triple2) -> (rule4 % int2)) triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((triple6) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple8 triple10) -> (rule7 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple8 ((triple8 ((triple11 triple9) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
((triple11 triple9) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple8 triple10) -> (rule7 % int2)) triple11) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((((triple8 triple10) -> (rule7 % int3)) triple9) -> (rule4 % int2)) triple9) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((((triple8 triple10) -> (rule7 % int3)) ((((triple8 triple10) -> (rule7 % int3)) triple9) -> (rule4 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
((triple13) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple13 triple14) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple1 triple4) -> (rule2 % int2))) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((triple4 triple2) -> (rule1 % int2))) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((triple1 ((triple1 triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((((((triple1 triple2) -> (rule4 % int3)) triple2) -> (rule1 % int2))) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
((((triple6) -> (rule6 % int2)) triple6) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((triple13) -> (rule3 % int2)) triple15) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple13) -> (rule3 % int4)) ((triple13 ((triple13 triple14) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
((((triple13) -> (rule3 % int4)) ((((triple13 triple14) -> (rule4 % int3)) triple14) -> (rule1 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Bob is green.
("Bob" "is" "green" "+")
((((triple6) -> (rule6 % int3)) ((((triple6) -> (rule6 % int3)) triple6) -> (rule5 % int2))) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
((((((triple6) -> (rule6 % int4)) ((((triple6) -> (rule6 % int4)) triple6) -> (rule5 % int3))) -> (rule7 % int2)) triple5) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4