The cat does not see the tiger. The rabbit does not see the cat. The rabbit visits the tiger. The squirrel is kind. The squirrel needs the cat. The squirrel does not need the rabbit. The squirrel sees the tiger. The squirrel visits the tiger. The tiger is green. The tiger is round. The tiger needs the rabbit. The tiger sees the squirrel. If something needs the tiger then it visits the tiger. If something sees the squirrel then it visits the tiger. If the tiger sees the cat and the cat is not green then the tiger visits the rabbit. If something sees the cat then the cat needs the rabbit. If something is green and it visits the tiger then the tiger sees the cat. If something is round and it needs the cat then it sees the squirrel. If something sees the tiger then it sees the squirrel. If the cat needs the rabbit then the cat sees the squirrel.
The cat does not see the tiger.
("cat" "sees" "tiger" "-")
The rabbit does not see the cat.
("rabbit" "sees" "cat" "-")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
The squirrel does not need the rabbit.
("squirrel" "needs" "rabbit" "-")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If something needs the tiger then it visits the tiger.
((("something" "needs" "tiger" "+")) -> ("something" "visits" "tiger" "+"))
If something sees the squirrel then it visits the tiger.
((("something" "sees" "squirrel" "+")) -> ("something" "visits" "tiger" "+"))
If the tiger sees the cat and the cat is not green then the tiger visits the rabbit.
((("tiger" "sees" "cat" "+") ("cat" "is" "green" "~")) -> ("tiger" "visits" "rabbit" "+"))
If something sees the cat then the cat needs the rabbit.
((("something" "sees" "cat" "+")) -> ("cat" "needs" "rabbit" "+"))
If something is green and it visits the tiger then the tiger sees the cat.
((("something" "is" "green" "+") ("something" "visits" "tiger" "+")) -> ("tiger" "sees" "cat" "+"))
If something is round and it needs the cat then it sees the squirrel.
((("something" "is" "round" "+") ("something" "needs" "cat" "+")) -> ("something" "sees" "squirrel" "+"))
If something sees the tiger then it sees the squirrel.
((("something" "sees" "tiger" "+")) -> ("something" "sees" "squirrel" "+"))
If the cat needs the rabbit then the cat sees the squirrel.
((("cat" "needs" "rabbit" "+")) -> ("cat" "sees" "squirrel" "+"))
The cat does not see the tiger.
True
1
proof
[(triple1)]
("cat" "sees" "tiger" "-")
triple1
The cat sees the tiger.
False
1
inv-proof
[(triple1)]
("cat" "sees" "tiger" "+")
triple1
The squirrel sees the squirrel.
True
2
proof
[(((triple7) -> rule7))]
("squirrel" "sees" "squirrel" "+")
((triple7) -> (rule7 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The tiger does not visit the tiger.
False
2
inv-proof
[(((triple12) -> rule2))]
("tiger" "visits" "tiger" "-")
((triple12) -> (rule2 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger sees the cat.
True
4
proof
[(((triple9 ((triple12) -> rule2)) -> rule5))]
("tiger" "sees" "cat" "+")
((triple9 ((triple12) -> (rule2 % int2))) -> (rule5 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger does not see the cat.
False
4
inv-proof
[(((triple9 ((triple12) -> rule2)) -> rule5))]
("tiger" "sees" "cat" "-")
((triple9 ((triple12) -> (rule2 % int2))) -> (rule5 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The cat needs the rabbit.
True
5
proof
[(((((triple9 ((triple12) -> rule2)) -> rule5)) -> rule4))]
("cat" "needs" "rabbit" "+")
((((triple9 ((triple12) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int3
The cat does not need the rabbit.
False
5
inv-proof
[(((((triple9 ((triple12) -> rule2)) -> rule5)) -> rule4))]
("cat" "needs" "rabbit" "-")
((((triple9 ((triple12) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int3
The cat sees the squirrel.
True
6
proof
[(((((((triple9 ((triple12) -> rule2)) -> rule5)) -> rule4)) -> rule8))]
("cat" "sees" "squirrel" "+")
((((((triple9 ((triple12) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int2
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int3
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int4
The cat does not see the squirrel.
False
6
inv-proof
[(((((((triple9 ((triple12) -> rule2)) -> rule5)) -> rule4)) -> rule8))]
("cat" "sees" "squirrel" "-")
((((((triple9 ((triple12) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int2
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int3
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int4
The cat visits the tiger.
True
7
proof
[(((((((((triple9 ((triple12) -> rule2)) -> rule5)) -> rule4)) -> rule8)) -> rule2))]
("cat" "visits" "tiger" "+")
((((((((triple9 ((triple12) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int2
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int3
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int4
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int5
The cat does not visit the tiger.
False
7
inv-proof
[(((((((((triple9 ((triple12) -> rule2)) -> rule5)) -> rule4)) -> rule8)) -> rule2))]
("cat" "visits" "tiger" "-")
((((((((triple9 ((triple12) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int2
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int3
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int4
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int5
The rabbit does not see the squirrel.
Unknown
inv-rconc
[@1: The rabbit sees the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "sees" "squirrel" "-")
The tiger visits the rabbit.
Unknown
rconc
[@1: The tiger visits the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "visits" "rabbit" "+")
The cat does not visit the squirrel.
Unknown
inv-random
[@0: The cat visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "squirrel" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
The tiger does not need the cat.
Unknown
inv-random
[@0: The tiger needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "cat" "-")
The rabbit is round.
Unknown
random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "+")
The squirrel is not green.
Unknown
inv-random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "-")
The rabbit is green.
Unknown
random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "+")
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The rabbit is blue.
Unknown
random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "+")
The squirrel is not blue.
Unknown
inv-random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "-")
The cat needs the squirrel.
Unknown
random
[@0: The cat needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "squirrel" "+")
@0: The cat does not see the tiger.[(triple1)] The rabbit does not see the cat.[(triple2)] The rabbit visits the tiger.[(triple3)] The squirrel does not need the rabbit.[(triple6)] The squirrel is kind.[(triple4)] The squirrel needs the cat.[(triple5)] The squirrel sees the tiger.[(triple7)] The squirrel visits the tiger.[(triple8 OR ((((triple7) -> rule7)) -> rule2))] The tiger is green.[(triple9)] The tiger is round.[(triple10)] The tiger needs the rabbit.[(triple11)] The tiger sees the squirrel.[(triple12)] @1: The squirrel sees the squirrel.[(((triple7) -> rule7))] The tiger visits the tiger.[(((triple12) -> rule2))] @2: The tiger sees the cat.[(((triple9 ((triple12) -> rule2)) -> rule5))] @3: The cat needs the rabbit.[(((((triple9 ((triple12) -> rule2)) -> rule5)) -> rule4))] @4: The cat sees the squirrel.[(((((((triple9 ((triple12) -> rule2)) -> rule5)) -> rule4)) -> rule8))] @5: The cat visits the tiger.[(((((((((triple9 ((triple12) -> rule2)) -> rule5)) -> rule4)) -> rule8)) -> rule2))]
The cat does not see the tiger.
("cat" "sees" "tiger" "-")
triple1
The rabbit does not see the cat.
("rabbit" "sees" "cat" "-")
triple2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple3
The squirrel does not need the rabbit.
("squirrel" "needs" "rabbit" "-")
triple6
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple4
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple5
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple7
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple8
((((triple7) -> (rule7 % int2))) -> (rule2 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
triple9
The tiger is round.
("tiger" "is" "round" "+")
triple10
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple11
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple12
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((triple7) -> (rule7 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple12) -> (rule2 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
((triple9 ((triple12) -> (rule2 % int2))) -> (rule5 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
((((triple9 ((triple12) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int3
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
((((((triple9 ((triple12) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int2
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int3
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int4
The cat visits the tiger.
("cat" "visits" "tiger" "+")
((((((((triple9 ((triple12) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int2
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int3
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int4
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int5