The cat does not chase the tiger. The cat needs the tiger. The tiger sees the cat. If someone needs the tiger and they are not kind then the tiger needs the cat. If the tiger chases the cat then the tiger is green. If someone is kind and they see the cat then the cat is cold. If someone sees the cat then they are cold. If someone needs the tiger and the tiger needs the cat then the tiger chases the cat. If someone sees the cat then they need the cat.
The cat does not chase the tiger.
("cat" "chases" "tiger" "-")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If someone needs the tiger and they are not kind then the tiger needs the cat.
((("someone" "needs" "tiger" "+") ("someone" "is" "kind" "~")) -> ("tiger" "needs" "cat" "+"))
If the tiger chases the cat then the tiger is green.
((("tiger" "chases" "cat" "+")) -> ("tiger" "is" "green" "+"))
If someone is kind and they see the cat then the cat is cold.
((("someone" "is" "kind" "+") ("someone" "sees" "cat" "+")) -> ("cat" "is" "cold" "+"))
If someone sees the cat then they are cold.
((("someone" "sees" "cat" "+")) -> ("someone" "is" "cold" "+"))
If someone needs the tiger and the tiger needs the cat then the tiger chases the cat.
((("someone" "needs" "tiger" "+") ("tiger" "needs" "cat" "+")) -> ("tiger" "chases" "cat" "+"))
If someone sees the cat then they need the cat.
((("someone" "sees" "cat" "+")) -> ("someone" "needs" "cat" "+"))
The tiger sees the cat.
True
1
proof
[(triple3)]
("tiger" "sees" "cat" "+")
triple3
The cat does not need the tiger.
False
1
inv-proof
[(triple2)]
("cat" "needs" "tiger" "-")
triple2
The tiger is cold.
True
2
proof
[(((triple3) -> rule4))]
("tiger" "is" "cold" "+")
((triple3) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is not cold.
False
2
inv-proof
[(((triple3) -> rule4))]
("tiger" "is" "cold" "-")
((triple3) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger chases the cat.
True
4
proof
[(((triple2 ((triple3) -> rule6)) -> rule5))]
("tiger" "chases" "cat" "+")
((triple2 ((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The tiger does not chase the cat.
False
4
inv-proof
[(((triple2 ((triple3) -> rule6)) -> rule5))]
("tiger" "chases" "cat" "-")
((triple2 ((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The tiger is green.
True
5
proof
[(((((triple2 ((triple3) -> rule6)) -> rule5)) -> rule2))]
("tiger" "is" "green" "+")
((((triple2 ((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int3
The tiger is not green.
False
5
inv-proof
[(((((triple2 ((triple3) -> rule6)) -> rule5)) -> rule2))]
("tiger" "is" "green" "-")
((((triple2 ((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int3
The cat is not cold.
Unknown
inv-rconc
[@1: The cat is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "cold" "-")
The cat needs the cat.
Unknown
rconc
[@1: The cat needs the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "needs" "cat" "+")
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
The cat is not blue.
Unknown
inv-random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "-")
The cat is red.
Unknown
random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "+")
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
@0: The cat does not chase the tiger.[(triple1)] The cat needs the tiger.[(triple2)] The tiger sees the cat.[(triple3)] @1: The tiger is cold.[(((triple3) -> rule4))] The tiger needs the cat.[(((triple3) -> rule6))] @2: The tiger chases the cat.[(((triple2 ((triple3) -> rule6)) -> rule5))] @3: The tiger is green.[(((((triple2 ((triple3) -> rule6)) -> rule5)) -> rule2))]
The cat does not chase the tiger.
("cat" "chases" "tiger" "-")
triple1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple2
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple3
The tiger is cold.
("tiger" "is" "cold" "+")
((triple3) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
((triple3) -> (rule6 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
((triple2 ((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
((((triple2 ((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int3