The squirrel visits the tiger. The tiger is not nice. If something visits the tiger and it eats the tiger then the tiger does not eat the squirrel. If the squirrel visits the tiger and the squirrel is young then the squirrel is round. If something visits the tiger then it eats the tiger. If the squirrel visits the tiger then the squirrel is kind. If the tiger visits the squirrel and the tiger is cold then the tiger does not like the squirrel. If the squirrel eats the tiger and the tiger does not eat the squirrel then the tiger is young. If something eats the squirrel and the squirrel does not eat the tiger then it is not cold. If something visits the tiger and the tiger is not young then it is nice.
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger is not nice.
("tiger" "is" "nice" "-")
If something visits the tiger and it eats the tiger then the tiger does not eat the squirrel.
((("something" "visits" "tiger" "+") ("something" "eats" "tiger" "+")) -> ("tiger" "eats" "squirrel" "-"))
If the squirrel visits the tiger and the squirrel is young then the squirrel is round.
((("squirrel" "visits" "tiger" "+") ("squirrel" "is" "young" "+")) -> ("squirrel" "is" "round" "+"))
If something visits the tiger then it eats the tiger.
((("something" "visits" "tiger" "+")) -> ("something" "eats" "tiger" "+"))
If the squirrel visits the tiger then the squirrel is kind.
((("squirrel" "visits" "tiger" "+")) -> ("squirrel" "is" "kind" "+"))
If the tiger visits the squirrel and the tiger is cold then the tiger does not like the squirrel.
((("tiger" "visits" "squirrel" "+") ("tiger" "is" "cold" "+")) -> ("tiger" "likes" "squirrel" "-"))
If the squirrel eats the tiger and the tiger does not eat the squirrel then the tiger is young.
((("squirrel" "eats" "tiger" "+") ("tiger" "eats" "squirrel" "~")) -> ("tiger" "is" "young" "+"))
If something eats the squirrel and the squirrel does not eat the tiger then it is not cold.
((("something" "eats" "squirrel" "+") ("squirrel" "eats" "tiger" "~")) -> ("something" "is" "cold" "-"))
If something visits the tiger and the tiger is not young then it is nice.
((("something" "visits" "tiger" "+") ("tiger" "is" "young" "~")) -> ("something" "is" "nice" "+"))
The squirrel visits the tiger.
True
1
proof
[(triple1)]
("squirrel" "visits" "tiger" "+")
triple1
The tiger is nice.
False
1
inv-proof
[(triple2)]
("tiger" "is" "nice" "+")
triple2
The squirrel eats the tiger.
True
2
proof
[(((triple1) -> rule3))]
("squirrel" "eats" "tiger" "+")
((triple1) -> (rule3 % int1))
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int1
The squirrel does not eat the tiger.
False
2
inv-proof
[(((triple1) -> rule3))]
("squirrel" "eats" "tiger" "-")
((triple1) -> (rule3 % int1))
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int1
The tiger does not eat the squirrel.
True
4
proof
[(((triple1 ((triple1) -> rule3)) -> rule1))]
("tiger" "eats" "squirrel" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The tiger does not eat the squirrel.
("tiger" "eats" "squirrel" "-")
int1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int2
The tiger eats the squirrel.
False
4
inv-proof
[(((triple1 ((triple1) -> rule3)) -> rule1))]
("tiger" "eats" "squirrel" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The tiger does not eat the squirrel.
("tiger" "eats" "squirrel" "-")
int1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int2
The tiger is young.
True
7
proof
[(((((triple1) -> rule3) ((triple1 ((triple1) -> rule3)) -> rule1)) -> rule6))]
("tiger" "is" "young" "+")
((((triple1) -> (rule3 % int3)) ((triple1 ((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger does not eat the squirrel.
("tiger" "eats" "squirrel" "-")
int2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int3
The tiger is not young.
False
7
inv-proof
[(((((triple1) -> rule3) ((triple1 ((triple1) -> rule3)) -> rule1)) -> rule6))]
("tiger" "is" "young" "-")
((((triple1) -> (rule3 % int3)) ((triple1 ((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger does not eat the squirrel.
("tiger" "eats" "squirrel" "-")
int2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int3
The squirrel is not round.
Unknown
inv-rconc
[@1: The squirrel is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "is" "round" "-")
The squirrel is nice.
Unknown
rconc
[@1: The squirrel is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "is" "nice" "+")
The tiger does not eat the tiger.
Unknown
inv-rconc
[@1: The tiger eats the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "eats" "tiger" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
The tiger does not like the squirrel.
Unknown
inv-random
[@0: The tiger likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "squirrel" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The squirrel is cold.
Unknown
random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "+")
@0: The squirrel visits the tiger.[(triple1)] The tiger is not nice.[(triple2)] @1: The squirrel eats the tiger.[(((triple1) -> rule3))] The squirrel is kind.[(((triple1) -> rule4))] @2: The tiger does not eat the squirrel.[(((triple1 ((triple1) -> rule3)) -> rule1))] @3: The tiger is young.[(((((triple1) -> rule3) ((triple1 ((triple1) -> rule3)) -> rule1)) -> rule6))]
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple1
The tiger is not nice.
("tiger" "is" "nice" "-")
triple2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
((triple1) -> (rule3 % int1))
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
((triple1) -> (rule4 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The tiger does not eat the squirrel.
("tiger" "eats" "squirrel" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The tiger does not eat the squirrel.
("tiger" "eats" "squirrel" "-")
int1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
((((triple1) -> (rule3 % int3)) ((triple1 ((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger does not eat the squirrel.
("tiger" "eats" "squirrel" "-")
int2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int3