Anne is round. Anne is white. Anne is young. Erin is green. Erin is smart. Gary is big. Gary is green. Gary is white. Harry is green. Harry is red. Harry is smart. Harry is young. All red, smart things are round. If something is green then it is red. If Erin is big and Erin is young then Erin is white. White things are young. If Anne is green then Anne is young. All smart, young things are big. If something is red then it is green. Big, smart things are round. All red, round things are young.
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
All red, smart things are round.
((("something" "is" "red" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
If something is green then it is red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If Erin is big and Erin is young then Erin is white.
((("Erin" "is" "big" "+") ("Erin" "is" "young" "+")) -> ("Erin" "is" "white" "+"))
White things are young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
If Anne is green then Anne is young.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "young" "+"))
All smart, young things are big.
((("something" "is" "smart" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
If something is red then it is green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
Big, smart things are round.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
All red, round things are young.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
Erin is green.
True
1
proof
[(triple4)]
("Erin" "is" "green" "+")
triple4
Gary is not green.
False
1
inv-proof
[(triple7)]
("Gary" "is" "green" "-")
triple7
Harry is round.
True
3
proof
[(((triple10 triple11) -> rule1) OR ((((triple9) -> rule2) triple11) -> rule1) OR ((((triple11 triple12) -> rule6) triple11) -> rule8))]
("Harry" "is" "round" "+")
((triple10 triple11) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple9) -> (rule2 % int2)) triple11) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple11 triple12) -> (rule6 % int2)) triple11) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Gary is not red.
False
2
inv-proof
[(((triple7) -> rule2))]
("Gary" "is" "red" "-")
((triple7) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Erin is round.
True
4
proof
[(((((triple4) -> rule2) triple5) -> rule1))]
("Erin" "is" "round" "+")
((((triple4) -> (rule2 % int2)) triple5) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not round.
False
4
inv-proof
[(((((triple4) -> rule2) triple5) -> rule1))]
("Erin" "is" "round" "-")
((((triple4) -> (rule2 % int2)) triple5) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is young.
True
7
proof
[(((((triple4) -> rule2) ((((triple4) -> rule2) triple5) -> rule1)) -> rule9))]
("Erin" "is" "young" "+")
((((triple4) -> (rule2 % int3)) ((((triple4) -> (rule2 % int3)) triple5) -> (rule1 % int2))) -> (rule9 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is not young.
False
7
inv-proof
[(((((triple4) -> rule2) ((((triple4) -> rule2) triple5) -> rule1)) -> rule9))]
("Erin" "is" "young" "-")
((((triple4) -> (rule2 % int3)) ((((triple4) -> (rule2 % int3)) triple5) -> (rule1 % int2))) -> (rule9 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is big.
True
9
proof
[(((triple5 ((((triple4) -> rule2) ((((triple4) -> rule2) triple5) -> rule1)) -> rule9)) -> rule6))]
("Erin" "is" "big" "+")
((triple5 ((((triple4) -> (rule2 % int4)) ((((triple4) -> (rule2 % int4)) triple5) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
Erin is not big.
False
9
inv-proof
[(((triple5 ((((triple4) -> rule2) ((((triple4) -> rule2) triple5) -> rule1)) -> rule9)) -> rule6))]
("Erin" "is" "big" "-")
((triple5 ((((triple4) -> (rule2 % int4)) ((((triple4) -> (rule2 % int4)) triple5) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
Erin is white.
True
17
proof
[(((((triple5 ((((triple4) -> rule2) ((((triple4) -> rule2) triple5) -> rule1)) -> rule9)) -> rule6) ((((triple4) -> rule2) ((((triple4) -> rule2) triple5) -> rule1)) -> rule9)) -> rule3))]
("Erin" "is" "white" "+")
((((triple5 ((((triple4) -> (rule2 % int5)) ((((triple4) -> (rule2 % int5)) triple5) -> (rule1 % int4))) -> (rule9 % int3))) -> (rule6 % int2)) ((((triple4) -> (rule2 % int5)) ((((triple4) -> (rule2 % int5)) triple5) -> (rule1 % int4))) -> (rule9 % int3))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Erin is red.
("Erin" "is" "red" "+")
int5
Erin is not white.
False
17
inv-proof
[(((((triple5 ((((triple4) -> rule2) ((((triple4) -> rule2) triple5) -> rule1)) -> rule9)) -> rule6) ((((triple4) -> rule2) ((((triple4) -> rule2) triple5) -> rule1)) -> rule9)) -> rule3))]
("Erin" "is" "white" "-")
((((triple5 ((((triple4) -> (rule2 % int5)) ((((triple4) -> (rule2 % int5)) triple5) -> (rule1 % int4))) -> (rule9 % int3))) -> (rule6 % int2)) ((((triple4) -> (rule2 % int5)) ((((triple4) -> (rule2 % int5)) triple5) -> (rule1 % int4))) -> (rule9 % int3))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Erin is red.
("Erin" "is" "red" "+")
int5
Anne is not red.
Unknown
inv-rconc
[@2: Anne is red.[CWA. Example of deepest failure = (rule2 <- rule7 <- FAIL)]]
("Anne" "is" "red" "-")
Gary is round.
Unknown
rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "round" "+")
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "big" "-")
Anne is green.
Unknown
rconc
[@2: Anne is green.[CWA. Example of deepest failure = (rule7 <- rule2 <- FAIL)]]
("Anne" "is" "green" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Anne is round.[(triple1)] Anne is white.[(triple2)] Anne is young.[(triple3 OR ((triple2) -> rule4))] Erin is green.[(triple4)] Erin is smart.[(triple5)] Gary is big.[(triple6)] Gary is green.[(triple7)] Gary is white.[(triple8)] Harry is green.[(triple9 OR ((triple10) -> rule7))] Harry is red.[(triple10 OR ((triple9) -> rule2))] Harry is smart.[(triple11)] Harry is young.[(triple12 OR ((triple10 ((triple10 triple11) -> rule1)) -> rule9) OR ((((triple9) -> rule2) ((triple10 triple11) -> rule1)) -> rule9) OR ((triple10 ((((triple9) -> rule2) triple11) -> rule1)) -> rule9) OR ((((triple9) -> rule2) ((((triple9) -> rule2) triple11) -> rule1)) -> rule9))] @1: Erin is red.[(((triple4) -> rule2))] Gary is red.[(((triple7) -> rule2))] Gary is young.[(((triple8) -> rule4))] Harry is big.[(((triple11 triple12) -> rule6) OR ((triple11 ((triple10 ((triple10 triple11) -> rule1)) -> rule9)) -> rule6) OR ((triple11 ((((triple9) -> rule2) ((triple10 triple11) -> rule1)) -> rule9)) -> rule6) OR ((triple11 ((triple10 ((((triple9) -> rule2) triple11) -> rule1)) -> rule9)) -> rule6) OR ((triple11 ((((triple9) -> rule2) ((((triple9) -> rule2) triple11) -> rule1)) -> rule9)) -> rule6))] Harry is round.[(((triple10 triple11) -> rule1) OR ((((triple9) -> rule2) triple11) -> rule1) OR ((((triple11 triple12) -> rule6) triple11) -> rule8))] @2: Erin is round.[(((((triple4) -> rule2) triple5) -> rule1))] @3: Erin is young.[(((((triple4) -> rule2) ((((triple4) -> rule2) triple5) -> rule1)) -> rule9))] @4: Erin is big.[(((triple5 ((((triple4) -> rule2) ((((triple4) -> rule2) triple5) -> rule1)) -> rule9)) -> rule6))] @5: Erin is white.[(((((triple5 ((((triple4) -> rule2) ((((triple4) -> rule2) triple5) -> rule1)) -> rule9)) -> rule6) ((((triple4) -> rule2) ((((triple4) -> rule2) triple5) -> rule1)) -> rule9)) -> rule3))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
((triple2) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple4
Erin is smart.
("Erin" "is" "smart" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple7
Gary is white.
("Gary" "is" "white" "+")
triple8
Harry is green.
("Harry" "is" "green" "+")
triple9
((triple10) -> (rule7 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple10
((triple9) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
((triple10 ((triple10 triple11) -> (rule1 % int2))) -> (rule9 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((((triple9) -> (rule2 % int3)) ((triple10 triple11) -> (rule1 % int2))) -> (rule9 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
((triple10 ((((triple9) -> (rule2 % int3)) triple11) -> (rule1 % int2))) -> (rule9 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
((((triple9) -> (rule2 % int3)) ((((triple9) -> (rule2 % int3)) triple11) -> (rule1 % int2))) -> (rule9 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
((triple4) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple7) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple8) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple11 triple12) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple11 ((triple10 ((triple10 triple11) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
((triple11 ((((triple9) -> (rule2 % int4)) ((triple10 triple11) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4
((triple11 ((triple10 ((((triple9) -> (rule2 % int4)) triple11) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4
((triple11 ((((triple9) -> (rule2 % int4)) ((((triple9) -> (rule2 % int4)) triple11) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4
Harry is round.
("Harry" "is" "round" "+")
((triple10 triple11) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple9) -> (rule2 % int2)) triple11) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple11 triple12) -> (rule6 % int2)) triple11) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((((triple4) -> (rule2 % int2)) triple5) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((((triple4) -> (rule2 % int3)) ((((triple4) -> (rule2 % int3)) triple5) -> (rule1 % int2))) -> (rule9 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
((triple5 ((((triple4) -> (rule2 % int4)) ((((triple4) -> (rule2 % int4)) triple5) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
((((triple5 ((((triple4) -> (rule2 % int5)) ((((triple4) -> (rule2 % int5)) triple5) -> (rule1 % int4))) -> (rule9 % int3))) -> (rule6 % int2)) ((((triple4) -> (rule2 % int5)) ((((triple4) -> (rule2 % int5)) triple5) -> (rule1 % int4))) -> (rule9 % int3))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Erin is red.
("Erin" "is" "red" "+")
int5