The cow visits the squirrel. The squirrel is big. If the cow visits the squirrel then the cow eats the squirrel. If the cow eats the squirrel and the cow likes the squirrel then the cow is rough. If someone likes the cow then the cow eats the squirrel. If the squirrel is big and the squirrel is rough then the squirrel likes the cow. If someone visits the cow then they visit the squirrel. If someone is rough and they eat the squirrel then they like the cow. If someone eats the squirrel then they visit the cow. If someone eats the squirrel then they visit the squirrel.
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
If the cow visits the squirrel then the cow eats the squirrel.
((("cow" "visits" "squirrel" "+")) -> ("cow" "eats" "squirrel" "+"))
If the cow eats the squirrel and the cow likes the squirrel then the cow is rough.
((("cow" "eats" "squirrel" "+") ("cow" "likes" "squirrel" "+")) -> ("cow" "is" "rough" "+"))
If someone likes the cow then the cow eats the squirrel.
((("someone" "likes" "cow" "+")) -> ("cow" "eats" "squirrel" "+"))
If the squirrel is big and the squirrel is rough then the squirrel likes the cow.
((("squirrel" "is" "big" "+") ("squirrel" "is" "rough" "+")) -> ("squirrel" "likes" "cow" "+"))
If someone visits the cow then they visit the squirrel.
((("someone" "visits" "cow" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone is rough and they eat the squirrel then they like the cow.
((("someone" "is" "rough" "+") ("someone" "eats" "squirrel" "+")) -> ("someone" "likes" "cow" "+"))
If someone eats the squirrel then they visit the cow.
((("someone" "eats" "squirrel" "+")) -> ("someone" "visits" "cow" "+"))
If someone eats the squirrel then they visit the squirrel.
((("someone" "eats" "squirrel" "+")) -> ("someone" "visits" "squirrel" "+"))
The squirrel is big.
True
1
proof
[(triple2)]
("squirrel" "is" "big" "+")
triple2
The cow does not visit the squirrel.
False
1
inv-proof
[(triple1)]
("cow" "visits" "squirrel" "-")
triple1
The cow eats the squirrel.
True
2
proof
[(((triple1) -> rule1))]
("cow" "eats" "squirrel" "+")
((triple1) -> (rule1 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The cow does not eat the squirrel.
False
2
inv-proof
[(((triple1) -> rule1))]
("cow" "eats" "squirrel" "-")
((triple1) -> (rule1 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The cow is not rough.
Unknown
inv-rconc
[@1: The cow is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "rough" "-")
The squirrel visits the cow.
Unknown
rconc
[@1: The squirrel visits the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "visits" "cow" "+")
The squirrel is not red.
Unknown
inv-random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "-")
The squirrel is round.
Unknown
random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "+")
@0: The cow visits the squirrel.[(triple1)] The squirrel is big.[(triple2)] @1: The cow eats the squirrel.[(((triple1) -> rule1))] @2: The cow visits the cow.[(((((triple1) -> rule1)) -> rule7))]
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
triple1
The squirrel is big.
("squirrel" "is" "big" "+")
triple2
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
((triple1) -> (rule1 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int2