The cat eats the squirrel. The cat sees the squirrel. The cow eats the cat. The cow eats the squirrel. The cow is round. The cow likes the cat. The cow sees the cat. The squirrel eats the cow. The squirrel is round. The squirrel likes the cat. The squirrel likes the cow. The squirrel sees the cat. If something sees the cat and the cat eats the cow then it eats the cat. If something sees the squirrel then it is nice. If something sees the squirrel then it sees the cow. If something sees the squirrel and the squirrel sees the cow then it sees the cow. If something sees the cow then it eats the cow. If something eats the cow then the cow eats the cat.
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
The cow is round.
("cow" "is" "round" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
If something sees the cat and the cat eats the cow then it eats the cat.
((("something" "sees" "cat" "+") ("cat" "eats" "cow" "+")) -> ("something" "eats" "cat" "+"))
If something sees the squirrel then it is nice.
((("something" "sees" "squirrel" "+")) -> ("something" "is" "nice" "+"))
If something sees the squirrel then it sees the cow.
((("something" "sees" "squirrel" "+")) -> ("something" "sees" "cow" "+"))
If something sees the squirrel and the squirrel sees the cow then it sees the cow.
((("something" "sees" "squirrel" "+") ("squirrel" "sees" "cow" "+")) -> ("something" "sees" "cow" "+"))
If something sees the cow then it eats the cow.
((("something" "sees" "cow" "+")) -> ("something" "eats" "cow" "+"))
If something eats the cow then the cow eats the cat.
((("something" "eats" "cow" "+")) -> ("cow" "eats" "cat" "+"))
The squirrel likes the cow.
True
1
proof
[(triple11)]
("squirrel" "likes" "cow" "+")
triple11
The cow does not see the cat.
False
1
inv-proof
[(triple7)]
("cow" "sees" "cat" "-")
triple7
The cat sees the cow.
True
2
proof
[(((triple2) -> rule3))]
("cat" "sees" "cow" "+")
((triple2) -> (rule3 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The cat is not nice.
False
2
inv-proof
[(((triple2) -> rule2))]
("cat" "is" "nice" "-")
((triple2) -> (rule2 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat eats the cow.
True
3
proof
[(((((triple2) -> rule3)) -> rule5))]
("cat" "eats" "cow" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
int2
The cat does not eat the cow.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule5))]
("cat" "eats" "cow" "-")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
int2
The squirrel eats the cat.
True
5
proof
[(((triple12 ((((triple2) -> rule3)) -> rule5)) -> rule1))]
("squirrel" "eats" "cat" "+")
((triple12 ((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The cat sees the cow.
("cat" "sees" "cow" "+")
int3
The squirrel does not eat the cat.
False
5
inv-proof
[(((triple12 ((((triple2) -> rule3)) -> rule5)) -> rule1))]
("squirrel" "eats" "cat" "-")
((triple12 ((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The cat sees the cow.
("cat" "sees" "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 cow eats the cow.
Unknown
rconc
[@2: The cow eats the cow.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("cow" "eats" "cow" "+")
The cat does not eat the cat.
Unknown
inv-rconc
[@1: The cat eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "eats" "cat" "-")
The cow sees the cow.
Unknown
rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "sees" "cow" "+")
The squirrel does not see the squirrel.
Unknown
inv-random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "-")
The cat is cold.
Unknown
random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "+")
The cow is not young.
Unknown
inv-random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
@0: The cat eats the squirrel.[(triple1)] The cat sees the squirrel.[(triple2)] The cow eats the cat.[(triple3 OR ((triple8) -> rule6) OR ((((((triple2) -> rule3)) -> rule5)) -> rule6) OR ((triple7 ((((triple2) -> rule3)) -> rule5)) -> rule1))] The cow eats the squirrel.[(triple4)] The cow is round.[(triple5)] The cow likes the cat.[(triple6)] The cow sees the cat.[(triple7)] The squirrel eats the cow.[(triple8)] The squirrel is round.[(triple9)] The squirrel likes the cat.[(triple10)] The squirrel likes the cow.[(triple11)] The squirrel sees the cat.[(triple12)] @1: The cat is nice.[(((triple2) -> rule2))] The cat sees the cow.[(((triple2) -> rule3))] @2: The cat eats the cow.[(((((triple2) -> rule3)) -> rule5))] @3: The squirrel eats the cat.[(((triple12 ((((triple2) -> rule3)) -> rule5)) -> rule1))]
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple2
The cow eats the cat.
("cow" "eats" "cat" "+")
triple3
((triple8) -> (rule6 % int1))
The cow eats the cat.
("cow" "eats" "cat" "+")
int1
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cow eats the cat.
("cow" "eats" "cat" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The cat sees the cow.
("cat" "sees" "cow" "+")
int3
((triple7 ((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The cow eats the cat.
("cow" "eats" "cat" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The cat sees the cow.
("cat" "sees" "cow" "+")
int3
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
triple4
The cow is round.
("cow" "is" "round" "+")
triple5
The cow likes the cat.
("cow" "likes" "cat" "+")
triple6
The cow sees the cat.
("cow" "sees" "cat" "+")
triple7
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
triple8
The squirrel is round.
("squirrel" "is" "round" "+")
triple9
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple10
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
triple11
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple12
The cat is nice.
("cat" "is" "nice" "+")
((triple2) -> (rule2 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
((triple2) -> (rule3 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
int2
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
((triple12 ((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The cat sees the cow.
("cat" "sees" "cow" "+")
int3