The squirrel eats the tiger. The squirrel is big. The squirrel is cold. The squirrel is not nice. The squirrel does not like the tiger. The squirrel visits the tiger. The tiger likes the squirrel. If the squirrel visits the tiger and the tiger is red then the squirrel eats the tiger. If the tiger is cold and the squirrel does not visit the tiger then the squirrel eats the tiger. Rough, red things are big. If the squirrel does not like the tiger then the tiger eats the squirrel. If the squirrel likes the tiger and the squirrel does not eat the tiger then the tiger visits the squirrel. If something eats the tiger and the tiger eats the squirrel then it visits the squirrel. If something is nice and rough then it eats the squirrel. If something visits the squirrel then it eats the squirrel.
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is not nice.
("squirrel" "is" "nice" "-")
The squirrel does not like the tiger.
("squirrel" "likes" "tiger" "-")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
If the squirrel visits the tiger and the tiger is red then the squirrel eats the tiger.
((("squirrel" "visits" "tiger" "+") ("tiger" "is" "red" "+")) -> ("squirrel" "eats" "tiger" "+"))
If the tiger is cold and the squirrel does not visit the tiger then the squirrel eats the tiger.
((("tiger" "is" "cold" "+") ("squirrel" "visits" "tiger" "~")) -> ("squirrel" "eats" "tiger" "+"))
Rough, red things are big.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If the squirrel does not like the tiger then the tiger eats the squirrel.
((("squirrel" "likes" "tiger" "~")) -> ("tiger" "eats" "squirrel" "+"))
If the squirrel likes the tiger and the squirrel does not eat the tiger then the tiger visits the squirrel.
((("squirrel" "likes" "tiger" "+") ("squirrel" "eats" "tiger" "~")) -> ("tiger" "visits" "squirrel" "+"))
If something eats the tiger and the tiger eats the squirrel then it visits the squirrel.
((("something" "eats" "tiger" "+") ("tiger" "eats" "squirrel" "+")) -> ("something" "visits" "squirrel" "+"))
If something is nice and rough then it eats the squirrel.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "eats" "squirrel" "+"))
If something visits the squirrel then it eats the squirrel.
((("something" "visits" "squirrel" "+")) -> ("something" "eats" "squirrel" "+"))
The squirrel does not like the tiger.
True
1
proof
[(triple5)]
("squirrel" "likes" "tiger" "-")
triple5
The squirrel is not big.
False
1
inv-proof
[(triple2)]
("squirrel" "is" "big" "-")
triple2
The tiger eats the squirrel.
True
2
proof
[(((triple5) -> rule4))]
("tiger" "eats" "squirrel" "+")
((triple5) -> (rule4 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The tiger does not eat the squirrel.
False
2
inv-proof
[(((triple5) -> rule4))]
("tiger" "eats" "squirrel" "-")
((triple5) -> (rule4 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The squirrel visits the squirrel.
True
4
proof
[(((triple1 ((triple5) -> rule4)) -> rule6))]
("squirrel" "visits" "squirrel" "+")
((triple1 ((triple5) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int2
The squirrel does not visit the squirrel.
False
4
inv-proof
[(((triple1 ((triple5) -> rule4)) -> rule6))]
("squirrel" "visits" "squirrel" "-")
((triple1 ((triple5) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int2
The squirrel eats the squirrel.
True
5
proof
[(((((triple1 ((triple5) -> rule4)) -> rule6)) -> rule8))]
("squirrel" "eats" "squirrel" "+")
((((triple1 ((triple5) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int3
The squirrel does not eat the squirrel.
False
5
inv-proof
[(((((triple1 ((triple5) -> rule4)) -> rule6)) -> rule8))]
("squirrel" "eats" "squirrel" "-")
((((triple1 ((triple5) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int3
The tiger does not visit the squirrel.
Unknown
inv-rconc
[@1: The tiger visits the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "visits" "squirrel" "-")
The tiger is big.
Unknown
rconc
[@1: The tiger is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "big" "+")
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
The tiger is not nice.
Unknown
inv-random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The tiger is not red.
Unknown
inv-random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
@0: The squirrel does not like the tiger.[(triple5)] The squirrel eats the tiger.[(triple1)] The squirrel is big.[(triple2)] The squirrel is cold.[(triple3)] The squirrel is not nice.[(triple4)] The squirrel visits the tiger.[(triple6)] The tiger likes the squirrel.[(triple7)] @1: The tiger eats the squirrel.[(((triple5) -> rule4))] @2: The squirrel visits the squirrel.[(((triple1 ((triple5) -> rule4)) -> rule6))] @3: The squirrel eats the squirrel.[(((((triple1 ((triple5) -> rule4)) -> rule6)) -> rule8))]
The squirrel does not like the tiger.
("squirrel" "likes" "tiger" "-")
triple5
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple1
The squirrel is big.
("squirrel" "is" "big" "+")
triple2
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple3
The squirrel is not nice.
("squirrel" "is" "nice" "-")
triple4
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple6
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple7
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
((triple5) -> (rule4 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((triple1 ((triple5) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((((triple1 ((triple5) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int3