The bald eagle is cold. The cat is kind. The cat visits the mouse. The mouse eats the squirrel. The mouse is cold. The mouse sees the squirrel. The squirrel eats the bald eagle. The squirrel eats the cat. The squirrel eats the mouse. The squirrel is kind. The squirrel visits the cat. If someone visits the mouse and they see the bald eagle then the bald eagle is blue. If someone is blue then they see the cat. If someone eats the bald eagle and the bald eagle sees the cat then the cat is cold. If someone eats the bald eagle then they visit the bald eagle. If someone is kind then they see the bald eagle. Cold people are round. If someone sees the bald eagle and they visit the bald eagle then they visit the cat. If someone is cold and they see the bald eagle then the bald eagle is kind. If someone eats the squirrel and the squirrel eats the mouse then they eat the mouse.
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel eats the bald eagle.
("squirrel" "eats" "bald eagle" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
If someone visits the mouse and they see the bald eagle then the bald eagle is blue.
((("someone" "visits" "mouse" "+") ("someone" "sees" "bald eagle" "+")) -> ("bald eagle" "is" "blue" "+"))
If someone is blue then they see the cat.
((("someone" "is" "blue" "+")) -> ("someone" "sees" "cat" "+"))
If someone eats the bald eagle and the bald eagle sees the cat then the cat is cold.
((("someone" "eats" "bald eagle" "+") ("bald eagle" "sees" "cat" "+")) -> ("cat" "is" "cold" "+"))
If someone eats the bald eagle then they visit the bald eagle.
((("someone" "eats" "bald eagle" "+")) -> ("someone" "visits" "bald eagle" "+"))
If someone is kind then they see the bald eagle.
((("someone" "is" "kind" "+")) -> ("someone" "sees" "bald eagle" "+"))
Cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If someone sees the bald eagle and they visit the bald eagle then they visit the cat.
((("someone" "sees" "bald eagle" "+") ("someone" "visits" "bald eagle" "+")) -> ("someone" "visits" "cat" "+"))
If someone is cold and they see the bald eagle then the bald eagle is kind.
((("someone" "is" "cold" "+") ("someone" "sees" "bald eagle" "+")) -> ("bald eagle" "is" "kind" "+"))
If someone eats the squirrel and the squirrel eats the mouse then they eat the mouse.
((("someone" "eats" "squirrel" "+") ("squirrel" "eats" "mouse" "+")) -> ("someone" "eats" "mouse" "+"))
The mouse sees the squirrel.
True
1
proof
[(triple6)]
("mouse" "sees" "squirrel" "+")
triple6
The squirrel does not visit the cat.
False
1
inv-proof
[(triple11 OR ((((triple10) -> rule5) ((triple7) -> rule4)) -> rule7))]
("squirrel" "visits" "cat" "-")
triple11
((((triple10) -> (rule5 % int3)) ((triple7) -> (rule4 % int2))) -> (rule7 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The squirrel visits the bald eagle.
("squirrel" "visits" "bald eagle" "+")
int2
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int3
The squirrel sees the bald eagle.
True
2
proof
[(((triple10) -> rule5))]
("squirrel" "sees" "bald eagle" "+")
((triple10) -> (rule5 % int1))
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int1
The bald eagle is not round.
False
2
inv-proof
[(((triple1) -> rule6))]
("bald eagle" "is" "round" "-")
((triple1) -> (rule6 % int1))
The bald eagle is round.
("bald eagle" "is" "round" "+")
int1
The bald eagle is blue.
True
4
proof
[(((triple3 ((triple2) -> rule5)) -> rule1))]
("bald eagle" "is" "blue" "+")
((triple3 ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int2
The bald eagle is not blue.
False
4
inv-proof
[(((triple3 ((triple2) -> rule5)) -> rule1))]
("bald eagle" "is" "blue" "-")
((triple3 ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int2
The bald eagle sees the cat.
True
5
proof
[(((((triple3 ((triple2) -> rule5)) -> rule1)) -> rule2))]
("bald eagle" "sees" "cat" "+")
((((triple3 ((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int1
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int2
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int3
The bald eagle does not see the cat.
False
5
inv-proof
[(((((triple3 ((triple2) -> rule5)) -> rule1)) -> rule2))]
("bald eagle" "sees" "cat" "-")
((((triple3 ((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int1
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int2
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int3
The cat is cold.
True
7
proof
[(((triple7 ((((triple3 ((triple2) -> rule5)) -> rule1)) -> rule2)) -> rule3))]
("cat" "is" "cold" "+")
((triple7 ((((triple3 ((triple2) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int2
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int3
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int4
The cat is not cold.
False
7
inv-proof
[(((triple7 ((((triple3 ((triple2) -> rule5)) -> rule1)) -> rule2)) -> rule3))]
("cat" "is" "cold" "-")
((triple7 ((((triple3 ((triple2) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int2
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int3
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int4
The cat is round.
True
8
proof
[(((((triple7 ((((triple3 ((triple2) -> rule5)) -> rule1)) -> rule2)) -> rule3)) -> rule6))]
("cat" "is" "round" "+")
((((triple7 ((((triple3 ((triple2) -> (rule5 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int3
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int4
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int5
The cat is not round.
False
8
inv-proof
[(((((triple7 ((((triple3 ((triple2) -> rule5)) -> rule1)) -> rule2)) -> rule3)) -> rule6))]
("cat" "is" "round" "-")
((((triple7 ((((triple3 ((triple2) -> (rule5 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int3
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int4
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int5
The bald eagle does not visit the cat.
Unknown
inv-rconc
[@2: The bald eagle visits the cat.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("bald eagle" "visits" "cat" "-")
The mouse visits the cat.
Unknown
rconc
[@2: The mouse visits the cat.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("mouse" "visits" "cat" "+")
The mouse does not see the cat.
Unknown
inv-rconc
[@1: The mouse sees the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "sees" "cat" "-")
The squirrel sees the cat.
Unknown
rconc
[@1: The squirrel sees the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "sees" "cat" "+")
The cat does not see the cat.
Unknown
inv-rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "sees" "cat" "-")
The cat visits the cat.
Unknown
rconc
[@2: The cat visits the cat.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("cat" "visits" "cat" "+")
The cat does not visit the squirrel.
Unknown
inv-random
[@0: The cat visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "squirrel" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
The cat does not see the squirrel.
Unknown
inv-random
[@0: The cat sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "squirrel" "-")
The squirrel is red.
Unknown
random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "+")
The bald eagle does not eat the bald eagle.
Unknown
inv-random
[@0: The bald eagle eats the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "eats" "bald eagle" "-")
The bald eagle eats the cat.
Unknown
random
[@0: The bald eagle eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "eats" "cat" "+")
@0: The bald eagle is cold.[(triple1)] The cat is kind.[(triple2)] The cat visits the mouse.[(triple3)] The mouse eats the squirrel.[(triple4)] The mouse is cold.[(triple5)] The mouse sees the squirrel.[(triple6)] The squirrel eats the bald eagle.[(triple7)] The squirrel eats the cat.[(triple8)] The squirrel eats the mouse.[(triple9)] The squirrel is kind.[(triple10)] The squirrel visits the cat.[(triple11 OR ((((triple10) -> rule5) ((triple7) -> rule4)) -> rule7))] @1: The bald eagle is round.[(((triple1) -> rule6))] The cat sees the bald eagle.[(((triple2) -> rule5))] The mouse eats the mouse.[(((triple4 triple9) -> rule9))] The mouse is round.[(((triple5) -> rule6))] The squirrel sees the bald eagle.[(((triple10) -> rule5))] The squirrel visits the bald eagle.[(((triple7) -> rule4))] @2: The bald eagle is blue.[(((triple3 ((triple2) -> rule5)) -> rule1))] @3: The bald eagle sees the cat.[(((((triple3 ((triple2) -> rule5)) -> rule1)) -> rule2))] @4: The cat is cold.[(((triple7 ((((triple3 ((triple2) -> rule5)) -> rule1)) -> rule2)) -> rule3))] @5: The bald eagle is kind.[(((((triple7 ((((triple3 ((triple2) -> rule5)) -> rule1)) -> rule2)) -> rule3) ((triple2) -> rule5)) -> rule8))] The cat is round.[(((((triple7 ((((triple3 ((triple2) -> rule5)) -> rule1)) -> rule2)) -> rule3)) -> rule6))] @6: The bald eagle sees the bald eagle.[(((((((triple7 ((((triple3 ((triple2) -> rule5)) -> rule1)) -> rule2)) -> rule3) ((triple2) -> rule5)) -> rule8)) -> rule5))]
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple3
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple4
The mouse is cold.
("mouse" "is" "cold" "+")
triple5
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple6
The squirrel eats the bald eagle.
("squirrel" "eats" "bald eagle" "+")
triple7
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple8
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple9
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple10
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple11
((((triple10) -> (rule5 % int3)) ((triple7) -> (rule4 % int2))) -> (rule7 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The squirrel visits the bald eagle.
("squirrel" "visits" "bald eagle" "+")
int2
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int3
The bald eagle is round.
("bald eagle" "is" "round" "+")
((triple1) -> (rule6 % int1))
The bald eagle is round.
("bald eagle" "is" "round" "+")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
((triple2) -> (rule5 % int1))
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((triple4 triple9) -> (rule9 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
((triple5) -> (rule6 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
((triple10) -> (rule5 % int1))
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int1
The squirrel visits the bald eagle.
("squirrel" "visits" "bald eagle" "+")
((triple7) -> (rule4 % int1))
The squirrel visits the bald eagle.
("squirrel" "visits" "bald eagle" "+")
int1
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
((triple3 ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int2
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
((((triple3 ((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int1
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int2
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int3
The cat is cold.
("cat" "is" "cold" "+")
((triple7 ((((triple3 ((triple2) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int2
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int3
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int4
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
((((triple7 ((((triple3 ((triple2) -> (rule5 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule3 % int2)) ((triple2) -> (rule5 % int5))) -> (rule8 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int3
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int4
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int5
The cat is round.
("cat" "is" "round" "+")
((((triple7 ((((triple3 ((triple2) -> (rule5 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int3
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int4
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int5
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
((((((triple7 ((((triple3 ((triple2) -> (rule5 % int6))) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule3 % int3)) ((triple2) -> (rule5 % int6))) -> (rule8 % int2))) -> (rule5 % int1))
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int1
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int4
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int5
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int6