The squirrel is big. The tiger eats the squirrel. The tiger is cold. The tiger is kind. The tiger is nice. The tiger likes the squirrel. The tiger visits the squirrel. If someone is nice and they visit the squirrel then the squirrel is kind. If someone is big and they eat the tiger then they eat the squirrel. If someone eats the squirrel and they visit the squirrel then they are rough. If someone likes the tiger and they eat the squirrel then they are rough. If someone is rough and they eat the squirrel then the squirrel is cold. If the tiger likes the squirrel then the squirrel visits the tiger.
The squirrel is big.
("squirrel" "is" "big" "+")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If someone is nice and they visit the squirrel then the squirrel is kind.
((("someone" "is" "nice" "+") ("someone" "visits" "squirrel" "+")) -> ("squirrel" "is" "kind" "+"))
If someone is big and they eat the tiger then they eat the squirrel.
((("someone" "is" "big" "+") ("someone" "eats" "tiger" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone eats the squirrel and they visit the squirrel then they are rough.
((("someone" "eats" "squirrel" "+") ("someone" "visits" "squirrel" "+")) -> ("someone" "is" "rough" "+"))
If someone likes the tiger and they eat the squirrel then they are rough.
((("someone" "likes" "tiger" "+") ("someone" "eats" "squirrel" "+")) -> ("someone" "is" "rough" "+"))
If someone is rough and they eat the squirrel then the squirrel is cold.
((("someone" "is" "rough" "+") ("someone" "eats" "squirrel" "+")) -> ("squirrel" "is" "cold" "+"))
If the tiger likes the squirrel then the squirrel visits the tiger.
((("tiger" "likes" "squirrel" "+")) -> ("squirrel" "visits" "tiger" "+"))
The tiger is cold.
True
1
proof
[(triple3)]
("tiger" "is" "cold" "+")
triple3
The squirrel is not big.
False
1
inv-proof
[(triple1)]
("squirrel" "is" "big" "-")
triple1
The squirrel is kind.
True
3
proof
[(((triple5 triple7) -> rule1))]
("squirrel" "is" "kind" "+")
((triple5 triple7) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The tiger is not rough.
False
3
inv-proof
[(((triple2 triple7) -> rule3))]
("tiger" "is" "rough" "-")
((triple2 triple7) -> (rule3 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The squirrel is cold.
True
5
proof
[(((((triple2 triple7) -> rule3) triple2) -> rule5))]
("squirrel" "is" "cold" "+")
((((triple2 triple7) -> (rule3 % int2)) triple2) -> (rule5 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The squirrel is not cold.
False
5
inv-proof
[(((((triple2 triple7) -> rule3) triple2) -> rule5))]
("squirrel" "is" "cold" "-")
((((triple2 triple7) -> (rule3 % int2)) triple2) -> (rule5 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The squirrel is not rough.
Unknown
inv-rconc
[@1: The squirrel is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "rough" "-")
The squirrel eats the squirrel.
Unknown
rconc
[@1: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "eats" "squirrel" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
The squirrel is not nice.
Unknown
inv-random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "-")
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 is big.[(triple1)] The tiger eats the squirrel.[(triple2)] The tiger is cold.[(triple3)] The tiger is kind.[(triple4)] The tiger is nice.[(triple5)] The tiger likes the squirrel.[(triple6)] The tiger visits the squirrel.[(triple7)] @1: The squirrel is kind.[(((triple5 triple7) -> rule1))] The squirrel visits the tiger.[(((triple6) -> rule6))] The tiger is rough.[(((triple2 triple7) -> rule3))] @2: The squirrel is cold.[(((((triple2 triple7) -> rule3) triple2) -> rule5))]
The squirrel is big.
("squirrel" "is" "big" "+")
triple1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple2
The tiger is cold.
("tiger" "is" "cold" "+")
triple3
The tiger is kind.
("tiger" "is" "kind" "+")
triple4
The tiger is nice.
("tiger" "is" "nice" "+")
triple5
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple6
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple7
The squirrel is kind.
("squirrel" "is" "kind" "+")
((triple5 triple7) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
((triple6) -> (rule6 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
((triple2 triple7) -> (rule3 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
((((triple2 triple7) -> (rule3 % int2)) triple2) -> (rule5 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2