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