The cat eats the tiger. The cat is cold. The cat likes the tiger. The cat needs the tiger. The tiger eats the cat. The tiger is cold. The tiger is not red. The tiger is rough. The tiger likes the cat. The tiger needs the cat. If someone likes the tiger then the tiger likes the cat. If someone eats the cat then the cat is rough. If the cat is round and the cat eats the tiger then the cat needs the tiger. Rough people are round. If the cat is rough and the cat is not nice then the cat eats the tiger. If someone is cold and they do not like the cat then the cat is red.
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is not red.
("tiger" "is" "red" "-")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
If someone likes the tiger then the tiger likes the cat.
((("someone" "likes" "tiger" "+")) -> ("tiger" "likes" "cat" "+"))
If someone eats the cat then the cat is rough.
((("someone" "eats" "cat" "+")) -> ("cat" "is" "rough" "+"))
If the cat is round and the cat eats the tiger then the cat needs the tiger.
((("cat" "is" "round" "+") ("cat" "eats" "tiger" "+")) -> ("cat" "needs" "tiger" "+"))
Rough people are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
If the cat is rough and the cat is not nice then the cat eats the tiger.
((("cat" "is" "rough" "+") ("cat" "is" "nice" "~")) -> ("cat" "eats" "tiger" "+"))
If someone is cold and they do not like the cat then the cat is red.
((("someone" "is" "cold" "+") ("someone" "likes" "cat" "~")) -> ("cat" "is" "red" "+"))
The cat is cold.
True
1
proof
[(triple2)]
("cat" "is" "cold" "+")
triple2
The tiger is not cold.
False
1
inv-proof
[(triple6)]
("tiger" "is" "cold" "-")
triple6
The tiger is round.
True
2
proof
[(((triple8) -> rule4))]
("tiger" "is" "round" "+")
((triple8) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The cat is not rough.
False
2
inv-proof
[(((triple5) -> rule2))]
("cat" "is" "rough" "-")
((triple5) -> (rule2 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is round.
True
3
proof
[(((((triple5) -> rule2)) -> rule4))]
("cat" "is" "round" "+")
((((triple5) -> (rule2 % int2))) -> (rule4 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat is not round.
False
3
inv-proof
[(((((triple5) -> rule2)) -> rule4))]
("cat" "is" "round" "-")
((((triple5) -> (rule2 % int2))) -> (rule4 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat is not red.
Unknown
inv-rconc
[@1: The cat is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "is" "red" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
@0: The cat eats the tiger.[(triple1)] The cat is cold.[(triple2)] The cat likes the tiger.[(triple3)] The cat needs the tiger.[(triple4 OR ((((((triple5) -> rule2)) -> rule4) triple1) -> rule3))] The tiger eats the cat.[(triple5)] The tiger is cold.[(triple6)] The tiger is not red.[(triple7)] The tiger is rough.[(triple8)] The tiger likes the cat.[(triple9 OR ((triple3) -> rule1))] The tiger needs the cat.[(triple10)] @1: The cat is rough.[(((triple5) -> rule2))] The tiger is round.[(((triple8) -> rule4))] @2: The cat is round.[(((((triple5) -> rule2)) -> rule4))]
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple3
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple4
((((((triple5) -> (rule2 % int3))) -> (rule4 % int2)) triple1) -> (rule3 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple5
The tiger is cold.
("tiger" "is" "cold" "+")
triple6
The tiger is not red.
("tiger" "is" "red" "-")
triple7
The tiger is rough.
("tiger" "is" "rough" "+")
triple8
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple9
((triple3) -> (rule1 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple10
The cat is rough.
("cat" "is" "rough" "+")
((triple5) -> (rule2 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
((triple8) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The cat is round.
("cat" "is" "round" "+")
((((triple5) -> (rule2 % int2))) -> (rule4 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2