The squirrel chases the tiger. The squirrel eats the tiger. The squirrel visits the tiger. The tiger does not eat the squirrel. The tiger is cold. The tiger is green. The tiger is red. If something chases the squirrel and it visits the squirrel then the squirrel is rough. If something eats the tiger then the tiger visits the squirrel. If something visits the squirrel and the squirrel chases the tiger then the tiger visits the squirrel. If something is green then it chases the tiger. If the squirrel is red then the squirrel visits the tiger. If something chases the squirrel then it is not red.
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger does not eat the squirrel.
("tiger" "eats" "squirrel" "-")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is red.
("tiger" "is" "red" "+")
If something chases the squirrel and it visits the squirrel then the squirrel is rough.
((("something" "chases" "squirrel" "+") ("something" "visits" "squirrel" "+")) -> ("squirrel" "is" "rough" "+"))
If something eats the tiger then the tiger visits the squirrel.
((("something" "eats" "tiger" "+")) -> ("tiger" "visits" "squirrel" "+"))
If something visits the squirrel and the squirrel chases the tiger then the tiger visits the squirrel.
((("something" "visits" "squirrel" "+") ("squirrel" "chases" "tiger" "+")) -> ("tiger" "visits" "squirrel" "+"))
If something is green then it chases the tiger.
((("something" "is" "green" "+")) -> ("something" "chases" "tiger" "+"))
If the squirrel is red then the squirrel visits the tiger.
((("squirrel" "is" "red" "+")) -> ("squirrel" "visits" "tiger" "+"))
If something chases the squirrel then it is not red.
((("something" "chases" "squirrel" "+")) -> ("something" "is" "red" "-"))
The squirrel chases the tiger.
True
1
proof
[(triple1)]
("squirrel" "chases" "tiger" "+")
triple1
The tiger is not red.
False
1
inv-proof
[(triple7)]
("tiger" "is" "red" "-")
triple7
The tiger chases the tiger.
True
2
proof
[(((triple6) -> rule4))]
("tiger" "chases" "tiger" "+")
((triple6) -> (rule4 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger does not chase the tiger.
False
2
inv-proof
[(((triple6) -> rule4))]
("tiger" "chases" "tiger" "-")
((triple6) -> (rule4 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The squirrel is not rough.
Unknown
inv-rconc
[@1: The squirrel is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "rough" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
The squirrel is not cold.
Unknown
inv-random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
@0: The squirrel chases the tiger.[(triple1)] The squirrel eats the tiger.[(triple2)] The squirrel visits the tiger.[(triple3)] The tiger does not eat the squirrel.[(triple4)] The tiger is cold.[(triple5)] The tiger is green.[(triple6)] The tiger is red.[(triple7)] @1: The tiger chases the tiger.[(((triple6) -> rule4))] The tiger visits the squirrel.[(((triple2) -> rule2))]
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple2
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple3
The tiger does not eat the squirrel.
("tiger" "eats" "squirrel" "-")
triple4
The tiger is cold.
("tiger" "is" "cold" "+")
triple5
The tiger is green.
("tiger" "is" "green" "+")
triple6
The tiger is red.
("tiger" "is" "red" "+")
triple7
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((triple6) -> (rule4 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
((triple2) -> (rule2 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1