Anne is young. Bob is blue. Bob is furry. Bob is quiet. Bob is young. Erin is blue. Erin is furry. Erin is quiet. Erin is white. Erin is young. Harry is blue. Harry is young. If Anne is young then Anne is quiet. Cold, white people are quiet. All quiet people are furry. White people are blue. All young, quiet people are cold. If someone is blue then they are young. If someone is young and blue then they are red. All cold people are white.
Anne is young.
("Anne" "is" "young" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is young.
("Harry" "is" "young" "+")
If Anne is young then Anne is quiet.
((("Anne" "is" "young" "+")) -> ("Anne" "is" "quiet" "+"))
Cold, white people are quiet.
((("someone" "is" "cold" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
All quiet people are furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
White people are blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
All young, quiet people are cold.
((("someone" "is" "young" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
If someone is blue then they are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
If someone is young and blue then they are red.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
All cold people are white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
Anne is young.
True
1
proof
[(triple1)]
("Anne" "is" "young" "+")
triple1
Harry is not young.
False
1
inv-proof
[(triple12 OR ((triple11) -> rule6))]
("Harry" "is" "young" "-")
triple12
((triple11) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Bob is cold.
True
3
proof
[(((triple5 triple4) -> rule5) OR ((((triple2) -> rule6) triple4) -> rule5))]
("Bob" "is" "cold" "+")
((triple5 triple4) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple2) -> (rule6 % int2)) triple4) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is not red.
False
3
inv-proof
[(((triple5 triple2) -> rule7) OR ((((triple2) -> rule6) triple2) -> rule7) OR ((triple5 ((((((triple5 triple4) -> rule5)) -> rule8)) -> rule4)) -> rule7) OR ((((triple2) -> rule6) ((((((triple5 triple4) -> rule5)) -> rule8)) -> rule4)) -> rule7))]
("Bob" "is" "red" "-")
((triple5 triple2) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple2) -> (rule6 % int2)) triple2) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((triple5 ((((((triple5 triple4) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
((((triple2) -> (rule6 % int5)) ((((((triple5 triple4) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
Bob is young.
("Bob" "is" "young" "+")
int5
Anne is cold.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule5))]
("Anne" "is" "cold" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not furry.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("Anne" "is" "furry" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is white.
True
5
proof
[(((((triple1 ((triple1) -> rule1)) -> rule5)) -> rule8))]
("Anne" "is" "white" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is not white.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule1)) -> rule5)) -> rule8))]
("Anne" "is" "white" "-")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is blue.
True
6
proof
[(((((((triple1 ((triple1) -> rule1)) -> rule5)) -> rule8)) -> rule4))]
("Anne" "is" "blue" "+")
((((((triple1 ((triple1) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Anne is not blue.
False
6
inv-proof
[(((((((triple1 ((triple1) -> rule1)) -> rule5)) -> rule8)) -> rule4))]
("Anne" "is" "blue" "-")
((((((triple1 ((triple1) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Anne is red.
True
8
proof
[(((triple1 ((((((triple1 ((triple1) -> rule1)) -> rule5)) -> rule8)) -> rule4)) -> rule7))]
("Anne" "is" "red" "+")
((triple1 ((((((triple1 ((triple1) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is quiet.
("Anne" "is" "quiet" "+")
int5
Anne is not red.
False
8
inv-proof
[(((triple1 ((((((triple1 ((triple1) -> rule1)) -> rule5)) -> rule8)) -> rule4)) -> rule7))]
("Anne" "is" "red" "-")
((triple1 ((((((triple1 ((triple1) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is quiet.
("Anne" "is" "quiet" "+")
int5
Harry is not white.
Unknown
inv-rconc
[@3: Harry is white.[CWA. Example of deepest failure = (rule8 <- rule5 <- rule2 <- FAIL)]]
("Harry" "is" "white" "-")
Harry is cold.
Unknown
rconc
[@2: Harry is cold.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Harry" "is" "cold" "+")
Harry is not quiet.
Unknown
inv-rconc
[@2: Harry is quiet.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Harry" "is" "quiet" "-")
Harry is furry.
Unknown
rconc
[@3: Harry is furry.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule5 <- FAIL)]]
("Harry" "is" "furry" "+")
@0: Anne is young.[(triple1)] Bob is blue.[(triple2 OR ((((((triple5 triple4) -> rule5)) -> rule8)) -> rule4))] Bob is furry.[(triple3 OR ((triple4) -> rule3))] Bob is quiet.[(triple4)] Bob is young.[(triple5 OR ((triple2) -> rule6))] Erin is blue.[(triple6 OR ((triple9) -> rule4) OR ((((((triple10 triple8) -> rule5)) -> rule8)) -> rule4))] Erin is furry.[(triple7 OR ((triple8) -> rule3))] Erin is quiet.[(triple8)] Erin is white.[(triple9 OR ((((triple10 triple8) -> rule5)) -> rule8) OR ((((((triple6) -> rule6) triple8) -> rule5)) -> rule8))] Erin is young.[(triple10 OR ((triple6) -> rule6) OR ((((triple9) -> rule4)) -> rule6))] Harry is blue.[(triple11)] Harry is young.[(triple12 OR ((triple11) -> rule6))] @1: Anne is quiet.[(((triple1) -> rule1))] Bob is cold.[(((triple5 triple4) -> rule5) OR ((((triple2) -> rule6) triple4) -> rule5))] Bob is red.[(((triple5 triple2) -> rule7) OR ((((triple2) -> rule6) triple2) -> rule7) OR ((triple5 ((((((triple5 triple4) -> rule5)) -> rule8)) -> rule4)) -> rule7) OR ((((triple2) -> rule6) ((((((triple5 triple4) -> rule5)) -> rule8)) -> rule4)) -> rule7))] Erin is cold.[(((triple10 triple8) -> rule5) OR ((((triple6) -> rule6) triple8) -> rule5) OR ((((((triple9) -> rule4)) -> rule6) triple8) -> rule5))] Erin is red.[(((triple10 triple6) -> rule7) OR ((triple10 ((triple9) -> rule4)) -> rule7) OR ((((triple6) -> rule6) triple6) -> rule7) OR ((((triple6) -> rule6) ((triple9) -> rule4)) -> rule7) OR ((((((triple9) -> rule4)) -> rule6) triple6) -> rule7) OR ((((((triple9) -> rule4)) -> rule6) ((triple9) -> rule4)) -> rule7) OR ((triple10 ((((((triple10 triple8) -> rule5)) -> rule8)) -> rule4)) -> rule7) OR ((((triple6) -> rule6) ((((((triple10 triple8) -> rule5)) -> rule8)) -> rule4)) -> rule7) OR ((((((triple9) -> rule4)) -> rule6) ((((((triple10 triple8) -> rule5)) -> rule8)) -> rule4)) -> rule7))] Harry is red.[(((triple12 triple11) -> rule7) OR ((((triple11) -> rule6) triple11) -> rule7))] @2: Anne is cold.[(((triple1 ((triple1) -> rule1)) -> rule5))] Anne is furry.[(((((triple1) -> rule1)) -> rule3))] Bob is white.[(((((triple5 triple4) -> rule5)) -> rule8) OR ((((((triple2) -> rule6) triple4) -> rule5)) -> rule8))] @3: Anne is white.[(((((triple1 ((triple1) -> rule1)) -> rule5)) -> rule8))] @4: Anne is blue.[(((((((triple1 ((triple1) -> rule1)) -> rule5)) -> rule8)) -> rule4))] @5: Anne is red.[(((triple1 ((((((triple1 ((triple1) -> rule1)) -> rule5)) -> rule8)) -> rule4)) -> rule7))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((((((triple5 triple4) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
triple3
((triple4) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
triple5
((triple2) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple6
((triple9) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((((triple10 triple8) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
triple7
((triple8) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple8
Erin is white.
("Erin" "is" "white" "+")
triple9
((((triple10 triple8) -> (rule5 % int2))) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((((triple6) -> (rule6 % int3)) triple8) -> (rule5 % int2))) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
triple10
((triple6) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple9) -> (rule4 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
((triple11) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((triple5 triple4) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple2) -> (rule6 % int2)) triple4) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((triple5 triple2) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple2) -> (rule6 % int2)) triple2) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((triple5 ((((((triple5 triple4) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
((((triple2) -> (rule6 % int5)) ((((((triple5 triple4) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
Bob is young.
("Bob" "is" "young" "+")
int5
Erin is cold.
("Erin" "is" "cold" "+")
((triple10 triple8) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple6) -> (rule6 % int2)) triple8) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((((triple9) -> (rule4 % int3))) -> (rule6 % int2)) triple8) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
((triple10 triple6) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple10 ((triple9) -> (rule4 % int2))) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((((triple6) -> (rule6 % int2)) triple6) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((triple6) -> (rule6 % int3)) ((triple9) -> (rule4 % int2))) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
((((((triple9) -> (rule4 % int3))) -> (rule6 % int2)) triple6) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((((triple9) -> (rule4 % int3))) -> (rule6 % int2)) ((triple9) -> (rule4 % int3))) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((triple10 ((((((triple10 triple8) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
((((triple6) -> (rule6 % int5)) ((((((triple10 triple8) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
int5
((((((triple9) -> (rule4 % int5))) -> (rule6 % int4)) ((((((triple10 triple8) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule4 % int5))) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
int5
Harry is red.
("Harry" "is" "red" "+")
((triple12 triple11) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple11) -> (rule6 % int2)) triple11) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((((triple5 triple4) -> (rule5 % int2))) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((((triple2) -> (rule6 % int3)) triple4) -> (rule5 % int2))) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
((((((triple1 ((triple1) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Anne is red.
("Anne" "is" "red" "+")
((triple1 ((((((triple1 ((triple1) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is quiet.
("Anne" "is" "quiet" "+")
int5