The cow is blue. The squirrel is blue. The squirrel is cold. If someone visits the squirrel then they eat the squirrel. If someone is blue then they visit the squirrel. If someone visits the squirrel then the squirrel does not eat the cow. If the squirrel is not cold then the squirrel eats the cow. If someone eats the cow then the cow is blue. If someone sees the squirrel and they visit the cow then the cow is young. If someone visits the squirrel and they do not eat the cow then the squirrel visits the cow. If someone visits the squirrel and they do not eat the cow then they visit the cow.
The cow is blue.
("cow" "is" "blue" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
If someone visits the squirrel then they eat the squirrel.
((("someone" "visits" "squirrel" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone is blue then they visit the squirrel.
((("someone" "is" "blue" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone visits the squirrel then the squirrel does not eat the cow.
((("someone" "visits" "squirrel" "+")) -> ("squirrel" "eats" "cow" "-"))
If the squirrel is not cold then the squirrel eats the cow.
((("squirrel" "is" "cold" "~")) -> ("squirrel" "eats" "cow" "+"))
If someone eats the cow then the cow is blue.
((("someone" "eats" "cow" "+")) -> ("cow" "is" "blue" "+"))
If someone sees the squirrel and they visit the cow then the cow is young.
((("someone" "sees" "squirrel" "+") ("someone" "visits" "cow" "+")) -> ("cow" "is" "young" "+"))
If someone visits the squirrel and they do not eat the cow then the squirrel visits the cow.
((("someone" "visits" "squirrel" "+") ("someone" "eats" "cow" "~")) -> ("squirrel" "visits" "cow" "+"))
If someone visits the squirrel and they do not eat the cow then they visit the cow.
((("someone" "visits" "squirrel" "+") ("someone" "eats" "cow" "~")) -> ("someone" "visits" "cow" "+"))
The squirrel is cold.
True
1
proof
[(triple3)]
("squirrel" "is" "cold" "+")
triple3
The squirrel is not blue.
False
1
inv-proof
[(triple2)]
("squirrel" "is" "blue" "-")
triple2
The squirrel visits the squirrel.
True
2
proof
[(((triple2) -> rule2))]
("squirrel" "visits" "squirrel" "+")
((triple2) -> (rule2 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel does not visit the squirrel.
False
2
inv-proof
[(((triple2) -> rule2))]
("squirrel" "visits" "squirrel" "-")
((triple2) -> (rule2 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel does not eat the cow.
True
3
proof
[(((((triple1) -> rule2)) -> rule3) OR ((((triple2) -> rule2)) -> rule3))]
("squirrel" "eats" "cow" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel does not eat the cow.
("squirrel" "eats" "cow" "-")
int1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int2
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel does not eat the cow.
("squirrel" "eats" "cow" "-")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The squirrel eats the cow.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3) OR ((((triple2) -> rule2)) -> rule3))]
("squirrel" "eats" "cow" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel does not eat the cow.
("squirrel" "eats" "cow" "-")
int1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int2
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel does not eat the cow.
("squirrel" "eats" "cow" "-")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The squirrel visits the cow.
True
6
proof
[(((((triple2) -> rule2) ((((triple1) -> rule2)) -> rule3)) -> rule7) OR ((((triple2) -> rule2) ((((triple1) -> rule2)) -> rule3)) -> rule8) OR ((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule3)) -> rule7) OR ((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule3)) -> rule8))]
("squirrel" "visits" "cow" "+")
((((triple2) -> (rule2 % int4)) ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The squirrel does not eat the cow.
("squirrel" "eats" "cow" "-")
int2
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int3
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int4
((((triple2) -> (rule2 % int4)) ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The squirrel does not eat the cow.
("squirrel" "eats" "cow" "-")
int2
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int3
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int4
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The squirrel does not eat the cow.
("squirrel" "eats" "cow" "-")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int3
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The squirrel does not eat the cow.
("squirrel" "eats" "cow" "-")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int3
The squirrel does not visit the cow.
False
6
inv-proof
[(((((triple2) -> rule2) ((((triple1) -> rule2)) -> rule3)) -> rule7) OR ((((triple2) -> rule2) ((((triple1) -> rule2)) -> rule3)) -> rule8) OR ((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule3)) -> rule7) OR ((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule3)) -> rule8))]
("squirrel" "visits" "cow" "-")
((((triple2) -> (rule2 % int4)) ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The squirrel does not eat the cow.
("squirrel" "eats" "cow" "-")
int2
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int3
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int4
((((triple2) -> (rule2 % int4)) ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The squirrel does not eat the cow.
("squirrel" "eats" "cow" "-")
int2
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int3
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int4
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The squirrel does not eat the cow.
("squirrel" "eats" "cow" "-")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int3
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The squirrel does not eat the cow.
("squirrel" "eats" "cow" "-")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int3
The cow does not visit the cow.
Unknown
inv-rconc
[@1: The cow visits the cow.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "visits" "cow" "-")
The cow is young.
Unknown
rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "is" "young" "+")
The squirrel is not young.
Unknown
inv-random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
The cow does not see the squirrel.
Unknown
inv-random
[@0: The cow sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "squirrel" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
@0: The cow is blue.[(triple1)] The squirrel is blue.[(triple2)] The squirrel is cold.[(triple3)] @1: The cow visits the squirrel.[(((triple1) -> rule2))] The squirrel visits the squirrel.[(((triple2) -> rule2))] @2: The cow eats the squirrel.[(((((triple1) -> rule2)) -> rule1))] The squirrel does not eat the cow.[(((((triple1) -> rule2)) -> rule3) OR ((((triple2) -> rule2)) -> rule3))] The squirrel eats the squirrel.[(((((triple2) -> rule2)) -> rule1))] @3: The squirrel visits the cow.[(((((triple2) -> rule2) ((((triple1) -> rule2)) -> rule3)) -> rule7) OR ((((triple2) -> rule2) ((((triple1) -> rule2)) -> rule3)) -> rule8) OR ((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule3)) -> rule7) OR ((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule3)) -> rule8))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple2
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple3
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
((triple1) -> (rule2 % int1))
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((triple2) -> (rule2 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int2
The squirrel does not eat the cow.
("squirrel" "eats" "cow" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel does not eat the cow.
("squirrel" "eats" "cow" "-")
int1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int2
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel does not eat the cow.
("squirrel" "eats" "cow" "-")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
((((triple2) -> (rule2 % int4)) ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The squirrel does not eat the cow.
("squirrel" "eats" "cow" "-")
int2
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int3
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int4
((((triple2) -> (rule2 % int4)) ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The squirrel does not eat the cow.
("squirrel" "eats" "cow" "-")
int2
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int3
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int4
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The squirrel does not eat the cow.
("squirrel" "eats" "cow" "-")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int3
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The squirrel does not eat the cow.
("squirrel" "eats" "cow" "-")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int3