Anne is big. Anne is furry. Anne is white. Anne is young. Charlie is furry. Charlie is green. Charlie is smart. Charlie is young. Gary is big. Gary is green. Gary is smart. Gary is young. Big, smart people are blue. If Gary is blue then Gary is big. Furry people are big. If Charlie is furry and Charlie is blue then Charlie is young. If someone is white then they are furry. If someone is blue then they are white. If Charlie is green and Charlie is young then Charlie is furry. If someone is smart then they are big.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Big, smart people are blue.
((("someone" "is" "big" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
If Gary is blue then Gary is big.
((("Gary" "is" "blue" "+")) -> ("Gary" "is" "big" "+"))
Furry people are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
If Charlie is furry and Charlie is blue then Charlie is young.
((("Charlie" "is" "furry" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "young" "+"))
If someone is white then they are furry.
((("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
If someone is blue then they are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
If Charlie is green and Charlie is young then Charlie is furry.
((("Charlie" "is" "green" "+") ("Charlie" "is" "young" "+")) -> ("Charlie" "is" "furry" "+"))
If someone is smart then they are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
Charlie is furry.
True
1
proof
[(triple5 OR ((triple6 triple8) -> rule7) OR ((((((((triple7) -> rule8) triple7) -> rule1)) -> rule6)) -> rule5))]
("Charlie" "is" "furry" "+")
triple5
((triple6 triple8) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((((((triple7) -> (rule8 % int4)) triple7) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is not green.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "green" "-")
triple6
Charlie is big.
True
2
proof
[(((triple5) -> rule3) OR ((triple7) -> rule8) OR ((((triple6 triple8) -> rule7)) -> rule3))]
("Charlie" "is" "big" "+")
((triple5) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple7) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple6 triple8) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not big.
False
2
inv-proof
[(((triple5) -> rule3) OR ((triple7) -> rule8) OR ((((triple6 triple8) -> rule7)) -> rule3))]
("Charlie" "is" "big" "-")
((triple5) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple7) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple6 triple8) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Gary is white.
True
4
proof
[(((((triple9 triple11) -> rule1)) -> rule6) OR ((((((triple11) -> rule8) triple11) -> rule1)) -> rule6))]
("Gary" "is" "white" "+")
((((triple9 triple11) -> (rule1 % int2))) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((((triple11) -> (rule8 % int3)) triple11) -> (rule1 % int2))) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Charlie is not blue.
False
4
inv-proof
[(((((triple5) -> rule3) triple7) -> rule1) OR ((((triple7) -> rule8) triple7) -> rule1) OR ((((((triple6 triple8) -> rule7)) -> rule3) triple7) -> rule1))]
("Charlie" "is" "blue" "-")
((((triple5) -> (rule3 % int2)) triple7) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple7) -> (rule8 % int2)) triple7) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((((triple6 triple8) -> (rule7 % int3))) -> (rule3 % int2)) triple7) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Gary is furry.
True
5
proof
[(((((((triple9 triple11) -> rule1)) -> rule6)) -> rule5) OR ((((((((triple11) -> rule8) triple11) -> rule1)) -> rule6)) -> rule5))]
("Gary" "is" "furry" "+")
((((((triple9 triple11) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((((((((triple11) -> (rule8 % int4)) triple11) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Charlie is not white.
False
5
inv-proof
[(((((((triple5) -> rule3) triple7) -> rule1)) -> rule6) OR ((((((triple7) -> rule8) triple7) -> rule1)) -> rule6) OR ((((((((triple6 triple8) -> rule7)) -> rule3) triple7) -> rule1)) -> rule6))]
("Charlie" "is" "white" "-")
((((((triple5) -> (rule3 % int3)) triple7) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((((triple7) -> (rule8 % int3)) triple7) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((((((triple6 triple8) -> (rule7 % int4))) -> (rule3 % int3)) triple7) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "blue" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is big.[(triple1 OR ((triple2) -> rule3) OR ((((triple3) -> rule5)) -> rule3))] Anne is furry.[(triple2 OR ((triple3) -> rule5))] Anne is white.[(triple3)] Anne is young.[(triple4)] Charlie is furry.[(triple5 OR ((triple6 triple8) -> rule7) OR ((((((((triple7) -> rule8) triple7) -> rule1)) -> rule6)) -> rule5))] Charlie is green.[(triple6)] Charlie is smart.[(triple7)] Charlie is young.[(triple8 OR ((triple5 ((((triple5) -> rule3) triple7) -> rule1)) -> rule4) OR ((triple5 ((((triple7) -> rule8) triple7) -> rule1)) -> rule4) OR ((((((((((triple7) -> rule8) triple7) -> rule1)) -> rule6)) -> rule5) ((((triple5) -> rule3) triple7) -> rule1)) -> rule4) OR ((((((((((triple7) -> rule8) triple7) -> rule1)) -> rule6)) -> rule5) ((((triple7) -> rule8) triple7) -> rule1)) -> rule4))] Gary is big.[(triple9 OR ((triple11) -> rule8))] Gary is green.[(triple10)] Gary is smart.[(triple11)] Gary is young.[(triple12)] @1: Charlie is big.[(((triple5) -> rule3) OR ((triple7) -> rule8) OR ((((triple6 triple8) -> rule7)) -> rule3))] Gary is blue.[(((triple9 triple11) -> rule1) OR ((((triple11) -> rule8) triple11) -> rule1))] @2: Charlie is blue.[(((((triple5) -> rule3) triple7) -> rule1) OR ((((triple7) -> rule8) triple7) -> rule1) OR ((((((triple6 triple8) -> rule7)) -> rule3) triple7) -> rule1))] Gary is white.[(((((triple9 triple11) -> rule1)) -> rule6) OR ((((((triple11) -> rule8) triple11) -> rule1)) -> rule6))] @3: Charlie is white.[(((((((triple5) -> rule3) triple7) -> rule1)) -> rule6) OR ((((((triple7) -> rule8) triple7) -> rule1)) -> rule6) OR ((((((((triple6 triple8) -> rule7)) -> rule3) triple7) -> rule1)) -> rule6))] Gary is furry.[(((((((triple9 triple11) -> rule1)) -> rule6)) -> rule5) OR ((((((((triple11) -> rule8) triple11) -> rule1)) -> rule6)) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple2) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((triple3) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
Charlie is furry.
("Charlie" "is" "furry" "+")
triple5
((triple6 triple8) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((((((triple7) -> (rule8 % int4)) triple7) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is green.
("Charlie" "is" "green" "+")
triple6
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7
Charlie is young.
("Charlie" "is" "young" "+")
triple8
((triple5 ((((triple5) -> (rule3 % int3)) triple7) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((triple5 ((((triple7) -> (rule8 % int3)) triple7) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((((((((triple7) -> (rule8 % int5)) triple7) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule5 % int2)) ((((triple5) -> (rule3 % int5)) triple7) -> (rule1 % int4))) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is big.
("Charlie" "is" "big" "+")
int5
((((((((((triple7) -> (rule8 % int5)) triple7) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule5 % int2)) ((((triple7) -> (rule8 % int5)) triple7) -> (rule1 % int4))) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is big.
("Charlie" "is" "big" "+")
int5
Gary is big.
("Gary" "is" "big" "+")
triple9
((triple11) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
triple10
Gary is smart.
("Gary" "is" "smart" "+")
triple11
Gary is young.
("Gary" "is" "young" "+")
triple12
Charlie is big.
("Charlie" "is" "big" "+")
((triple5) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple7) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple6 triple8) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((triple9 triple11) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple11) -> (rule8 % int2)) triple11) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple5) -> (rule3 % int2)) triple7) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple7) -> (rule8 % int2)) triple7) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((((triple6 triple8) -> (rule7 % int3))) -> (rule3 % int2)) triple7) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
((((triple9 triple11) -> (rule1 % int2))) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((((triple11) -> (rule8 % int3)) triple11) -> (rule1 % int2))) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
((((((triple5) -> (rule3 % int3)) triple7) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((((triple7) -> (rule8 % int3)) triple7) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((((((triple6 triple8) -> (rule7 % int4))) -> (rule3 % int3)) triple7) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Gary is furry.
("Gary" "is" "furry" "+")
((((((triple9 triple11) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((((((((triple11) -> (rule8 % int4)) triple11) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4