Anne is big. Anne is blue. Anne is green. Anne is red. Anne is rough. Anne is round. Anne is smart. Gary is red. Gary is smart. Harry is big. Harry is blue. Harry is green. Harry is red. Harry is rough. Harry is smart. Blue things are round. If Harry is smart then Harry is blue. Big, smart things are red. Red, green things are rough. Rough things are smart. If something is red then it is smart. All big things are round. If something is green and red then it is round.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If Harry is smart then Harry is blue.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "blue" "+"))
Big, smart things are red.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Red, green things are rough.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If something is red then it is smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
All big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If something is green and red then it is round.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
Anne is red.
True
1
proof
[(triple4 OR ((triple1 triple7) -> rule3) OR ((triple1 ((triple5) -> rule5)) -> rule3))]
("Anne" "is" "red" "+")
triple4
((triple1 triple7) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple1 ((triple5) -> (rule5 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Harry is round.
True
2
proof
[(((triple10) -> rule7) OR ((triple11) -> rule1) OR ((triple12 triple13) -> rule8) OR ((((triple15) -> rule2)) -> rule1) OR ((triple12 ((triple10 triple15) -> rule3)) -> rule8) OR ((((((triple13) -> rule6)) -> rule2)) -> rule1) OR ((((((triple14) -> rule5)) -> rule2)) -> rule1) OR ((triple12 ((triple10 ((triple14) -> rule5)) -> rule3)) -> rule8) OR ((((((((triple13 triple12) -> rule4)) -> rule5)) -> rule2)) -> rule1))]
("Harry" "is" "round" "+")
((triple10) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((triple11) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((triple12 triple13) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple15) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((triple12 ((triple10 triple15) -> (rule3 % int2))) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((((triple13) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((((triple14) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((triple12 ((triple10 ((triple14) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((((((triple13 triple12) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is not round.
False
2
inv-proof
[(((triple10) -> rule7) OR ((triple11) -> rule1) OR ((triple12 triple13) -> rule8) OR ((((triple15) -> rule2)) -> rule1) OR ((triple12 ((triple10 triple15) -> rule3)) -> rule8) OR ((((((triple13) -> rule6)) -> rule2)) -> rule1) OR ((((((triple14) -> rule5)) -> rule2)) -> rule1) OR ((triple12 ((triple10 ((triple14) -> rule5)) -> rule3)) -> rule8) OR ((((((((triple13 triple12) -> rule4)) -> rule5)) -> rule2)) -> rule1))]
("Harry" "is" "round" "-")
((triple10) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((triple11) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((triple12 triple13) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple15) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((triple12 ((triple10 triple15) -> (rule3 % int2))) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((((triple13) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((((triple14) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((triple12 ((triple10 ((triple14) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((((((triple13 triple12) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "round" "-")
Gary is rough.
Unknown
rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "rough" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is green.[(triple3)] Anne is red.[(triple4 OR ((triple1 triple7) -> rule3) OR ((triple1 ((triple5) -> rule5)) -> rule3))] Anne is rough.[(triple5 OR ((triple4 triple3) -> rule4) OR ((((triple1 triple7) -> rule3) triple3) -> rule4))] Anne is round.[(triple6 OR ((triple1) -> rule7) OR ((triple2) -> rule1) OR ((triple3 triple4) -> rule8) OR ((triple3 ((triple1 triple7) -> rule3)) -> rule8) OR ((triple3 ((triple1 ((triple5) -> rule5)) -> rule3)) -> rule8))] Anne is smart.[(triple7 OR ((triple4) -> rule6) OR ((triple5) -> rule5) OR ((((triple4 triple3) -> rule4)) -> rule5))] Gary is red.[(triple8)] Gary is smart.[(triple9 OR ((triple8) -> rule6))] Harry is big.[(triple10)] Harry is blue.[(triple11 OR ((triple15) -> rule2) OR ((((triple13) -> rule6)) -> rule2) OR ((((triple14) -> rule5)) -> rule2) OR ((((((triple13 triple12) -> rule4)) -> rule5)) -> rule2))] Harry is green.[(triple12)] Harry is red.[(triple13 OR ((triple10 triple15) -> rule3) OR ((triple10 ((triple14) -> rule5)) -> rule3))] Harry is rough.[(triple14 OR ((triple13 triple12) -> rule4) OR ((((triple10 triple15) -> rule3) triple12) -> rule4))] Harry is smart.[(triple15 OR ((triple13) -> rule6) OR ((triple14) -> rule5) OR ((((triple13 triple12) -> rule4)) -> rule5))] @1: Harry is round.[(((triple10) -> rule7) OR ((triple11) -> rule1) OR ((triple12 triple13) -> rule8) OR ((((triple15) -> rule2)) -> rule1) OR ((triple12 ((triple10 triple15) -> rule3)) -> rule8) OR ((((((triple13) -> rule6)) -> rule2)) -> rule1) OR ((((((triple14) -> rule5)) -> rule2)) -> rule1) OR ((triple12 ((triple10 ((triple14) -> rule5)) -> rule3)) -> rule8) OR ((((((((triple13 triple12) -> rule4)) -> rule5)) -> rule2)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
((triple1 triple7) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple1 ((triple5) -> (rule5 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
triple5
((triple4 triple3) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple1 triple7) -> (rule3 % int2)) triple3) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
triple6
((triple1) -> (rule7 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple2) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple3 triple4) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple3 ((triple1 triple7) -> (rule3 % int2))) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((triple3 ((triple1 ((triple5) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
triple7
((triple4) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple5) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple4 triple3) -> (rule4 % int2))) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
triple8
Gary is smart.
("Gary" "is" "smart" "+")
triple9
((triple8) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple10
Harry is blue.
("Harry" "is" "blue" "+")
triple11
((triple15) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple13) -> (rule6 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple14) -> (rule5 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((((triple13 triple12) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
triple12
Harry is red.
("Harry" "is" "red" "+")
triple13
((triple10 triple15) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple10 ((triple14) -> (rule5 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
triple14
((triple13 triple12) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple10 triple15) -> (rule3 % int2)) triple12) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple15
((triple13) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple14) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple13 triple12) -> (rule4 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((triple10) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((triple11) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((triple12 triple13) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple15) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((triple12 ((triple10 triple15) -> (rule3 % int2))) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((((triple13) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((((triple14) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((triple12 ((triple10 ((triple14) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((((((triple13 triple12) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4