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