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