The cat is young. The cat needs the tiger. The tiger eats the cat. If someone eats the cat then they visit the tiger. If the cat is kind then the cat eats the tiger. If someone needs the cat then the cat visits the tiger. If someone needs the tiger then they need the cat. If someone needs the cat then the cat visits the tiger. If someone needs the tiger then the tiger is cold. If the cat eats the tiger then the cat visits the tiger. If someone is blue and they need the cat then the cat visits the tiger.
The cat is young.
("cat" "is" "young" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
If someone eats the cat then they visit the tiger.
((("someone" "eats" "cat" "+")) -> ("someone" "visits" "tiger" "+"))
If the cat is kind then the cat eats the tiger.
((("cat" "is" "kind" "+")) -> ("cat" "eats" "tiger" "+"))
If someone needs the cat then the cat visits the tiger.
((("someone" "needs" "cat" "+")) -> ("cat" "visits" "tiger" "+"))
If someone needs the tiger then they need the cat.
((("someone" "needs" "tiger" "+")) -> ("someone" "needs" "cat" "+"))
If someone needs the cat then the cat visits the tiger.
((("someone" "needs" "cat" "+")) -> ("cat" "visits" "tiger" "+"))
If someone needs the tiger then the tiger is cold.
((("someone" "needs" "tiger" "+")) -> ("tiger" "is" "cold" "+"))
If the cat eats the tiger then the cat visits the tiger.
((("cat" "eats" "tiger" "+")) -> ("cat" "visits" "tiger" "+"))
If someone is blue and they need the cat then the cat visits the tiger.
((("someone" "is" "blue" "+") ("someone" "needs" "cat" "+")) -> ("cat" "visits" "tiger" "+"))
The cat needs the tiger.
True
1
proof
[(triple2)]
("cat" "needs" "tiger" "+")
triple2
The cat is not young.
False
1
inv-proof
[(triple1)]
("cat" "is" "young" "-")
triple1
The tiger is cold.
True
2
proof
[(((triple2) -> rule6))]
("tiger" "is" "cold" "+")
((triple2) -> (rule6 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is not cold.
False
2
inv-proof
[(((triple2) -> rule6))]
("tiger" "is" "cold" "-")
((triple2) -> (rule6 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The cat does not eat the tiger.
Unknown
inv-rconc
[@1: The cat eats the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "eats" "tiger" "-")
The tiger needs the cat.
Unknown
rconc
[@1: The tiger needs the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "needs" "cat" "+")
The cat is not nice.
Unknown
inv-random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
@0: The cat is young.[(triple1)] The cat needs the tiger.[(triple2)] The tiger eats the cat.[(triple3)] @1: The cat needs the cat.[(((triple2) -> rule4))] The tiger is cold.[(((triple2) -> rule6))] The tiger visits the tiger.[(((triple3) -> rule1))] @2: The cat visits the tiger.[(((((triple2) -> rule4)) -> rule3) OR ((((triple2) -> rule4)) -> rule5))]
The cat is young.
("cat" "is" "young" "+")
triple1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple2
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple3
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple2) -> (rule4 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
((triple2) -> (rule6 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple3) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2