The cat does not chase the tiger. The cat does not eat the tiger. The cat is big. The cat needs the tiger. The tiger chases the cat. The tiger eats the cat. The tiger is not kind. The tiger is nice. The tiger is young. The tiger needs the cat. If something is cold then it eats the cat. If something eats the cat then the cat is not cold.
The cat does not chase the tiger.
("cat" "chases" "tiger" "-")
The cat does not eat the tiger.
("cat" "eats" "tiger" "-")
The cat is big.
("cat" "is" "big" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger is not kind.
("tiger" "is" "kind" "-")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
If something is cold then it eats the cat.
((("something" "is" "cold" "+")) -> ("something" "eats" "cat" "+"))
If something eats the cat then the cat is not cold.
((("something" "eats" "cat" "+")) -> ("cat" "is" "cold" "-"))
The tiger is nice.
True
1
proof
[(triple8)]
("tiger" "is" "nice" "+")
triple8
The tiger does not need the cat.
False
1
inv-proof
[(triple10)]
("tiger" "needs" "cat" "-")
triple10
The cat is not cold.
True
2
proof
[(((triple6) -> rule2))]
("cat" "is" "cold" "-")
((triple6) -> (rule2 % int1))
The cat is not cold.
("cat" "is" "cold" "-")
int1
The cat is cold.
False
2
inv-proof
[(((triple6) -> rule2))]
("cat" "is" "cold" "+")
((triple6) -> (rule2 % int1))
The cat is not cold.
("cat" "is" "cold" "-")
int1
The cat does not eat the cat.
Unknown
inv-rconc
[@1: The cat eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "eats" "cat" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
@0: The cat does not chase the tiger.[(triple1)] The cat does not eat the tiger.[(triple2)] The cat is big.[(triple3)] The cat needs the tiger.[(triple4)] The tiger chases the cat.[(triple5)] The tiger eats the cat.[(triple6)] The tiger is nice.[(triple8)] The tiger is not kind.[(triple7)] The tiger is young.[(triple9)] The tiger needs the cat.[(triple10)] @1: The cat is not cold.[(((triple6) -> rule2))]
The cat does not chase the tiger.
("cat" "chases" "tiger" "-")
triple1
The cat does not eat the tiger.
("cat" "eats" "tiger" "-")
triple2
The cat is big.
("cat" "is" "big" "+")
triple3
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple4
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple5
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple6
The tiger is nice.
("tiger" "is" "nice" "+")
triple8
The tiger is not kind.
("tiger" "is" "kind" "-")
triple7
The tiger is young.
("tiger" "is" "young" "+")
triple9
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple10
The cat is not cold.
("cat" "is" "cold" "-")
((triple6) -> (rule2 % int1))
The cat is not cold.
("cat" "is" "cold" "-")
int1