The cow likes the squirrel. The squirrel sees the cow. If someone sees the cow then they are not nice. If someone is blue then they are nice. If someone likes the squirrel then the squirrel does not like the cow. If the squirrel sees the cow then the cow is green. If the cow likes the squirrel and the squirrel does not like the cow then the squirrel is cold. If someone sees the cow and they do not like the cow then the cow sees the squirrel. If someone sees the squirrel then the squirrel eats the cow. If the cow likes the squirrel and the cow is not nice then the squirrel eats the cow.
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
If someone sees the cow then they are not nice.
((("someone" "sees" "cow" "+")) -> ("someone" "is" "nice" "-"))
If someone is blue then they are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If someone likes the squirrel then the squirrel does not like the cow.
((("someone" "likes" "squirrel" "+")) -> ("squirrel" "likes" "cow" "-"))
If the squirrel sees the cow then the cow is green.
((("squirrel" "sees" "cow" "+")) -> ("cow" "is" "green" "+"))
If the cow likes the squirrel and the squirrel does not like the cow then the squirrel is cold.
((("cow" "likes" "squirrel" "+") ("squirrel" "likes" "cow" "~")) -> ("squirrel" "is" "cold" "+"))
If someone sees the cow and they do not like the cow then the cow sees the squirrel.
((("someone" "sees" "cow" "+") ("someone" "likes" "cow" "~")) -> ("cow" "sees" "squirrel" "+"))
If someone sees the squirrel then the squirrel eats the cow.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "eats" "cow" "+"))
If the cow likes the squirrel and the cow is not nice then the squirrel eats the cow.
((("cow" "likes" "squirrel" "+") ("cow" "is" "nice" "~")) -> ("squirrel" "eats" "cow" "+"))
The squirrel sees the cow.
True
1
proof
[(triple2)]
("squirrel" "sees" "cow" "+")
triple2
The squirrel does not see the cow.
False
1
inv-proof
[(triple2)]
("squirrel" "sees" "cow" "-")
triple2
The cow is green.
True
2
proof
[(((triple2) -> rule4))]
("cow" "is" "green" "+")
((triple2) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The squirrel is nice.
False
2
inv-proof
[(((triple2) -> rule1))]
("squirrel" "is" "nice" "+")
((triple2) -> (rule1 % int1))
The squirrel is not nice.
("squirrel" "is" "nice" "-")
int1
The cow sees the squirrel.
True
4
proof
[(((triple2 ((triple1) -> rule3)) -> rule6))]
("cow" "sees" "squirrel" "+")
((triple2 ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The squirrel does not like the cow.
("squirrel" "likes" "cow" "-")
int2
The cow does not see the squirrel.
False
4
inv-proof
[(((triple2 ((triple1) -> rule3)) -> rule6))]
("cow" "sees" "squirrel" "-")
((triple2 ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The squirrel does not like the cow.
("squirrel" "likes" "cow" "-")
int2
The squirrel eats the cow.
True
5
proof
[(((((triple2 ((triple1) -> rule3)) -> rule6)) -> rule7))]
("squirrel" "eats" "cow" "+")
((((triple2 ((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int2
The squirrel does not like the cow.
("squirrel" "likes" "cow" "-")
int3
The squirrel does not eat the cow.
False
5
inv-proof
[(((((triple2 ((triple1) -> rule3)) -> rule6)) -> rule7))]
("squirrel" "eats" "cow" "-")
((((triple2 ((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int2
The squirrel does not like the cow.
("squirrel" "likes" "cow" "-")
int3
The cow is not nice.
Unknown
inv-rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "nice" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
The cow does not eat the squirrel.
Unknown
inv-random
[@0: The cow eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "squirrel" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
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 eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
The squirrel is not green.
Unknown
inv-random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
@0: The cow likes the squirrel.[(triple1)] The squirrel sees the cow.[(triple2)] @1: The cow is green.[(((triple2) -> rule4))] The squirrel does not like the cow.[(((triple1) -> rule3))] The squirrel is not nice.[(((triple2) -> rule1))] @2: The cow sees the squirrel.[(((triple2 ((triple1) -> rule3)) -> rule6))] The squirrel is cold.[(((triple1 ((triple1) -> rule3)) -> rule5))] @3: The squirrel eats the cow.[(((((triple2 ((triple1) -> rule3)) -> rule6)) -> rule7))]
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
triple1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
triple2
The cow is green.
("cow" "is" "green" "+")
((triple2) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The squirrel does not like the cow.
("squirrel" "likes" "cow" "-")
((triple1) -> (rule3 % int1))
The squirrel does not like the cow.
("squirrel" "likes" "cow" "-")
int1
The squirrel is not nice.
("squirrel" "is" "nice" "-")
((triple2) -> (rule1 % int1))
The squirrel is not nice.
("squirrel" "is" "nice" "-")
int1
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
((triple2 ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The squirrel does not like the cow.
("squirrel" "likes" "cow" "-")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel does not like the cow.
("squirrel" "likes" "cow" "-")
int2
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
((((triple2 ((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int2
The squirrel does not like the cow.
("squirrel" "likes" "cow" "-")
int3