The cat eats the cow. The cow is red. The rabbit eats the tiger. The tiger needs the cat. If the rabbit eats the tiger then the tiger is rough. If someone needs the tiger and they eat the cow then they need the rabbit. If someone visits the cat then they eat the cow. All cold people are rough. If someone is red then they are cold. If someone is rough then they visit the tiger. If someone visits the rabbit then the rabbit is rough. If someone needs the rabbit and the rabbit is red then they eat the cat.
The cat eats the cow.
("cat" "eats" "cow" "+")
The cow is red.
("cow" "is" "red" "+")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
If the rabbit eats the tiger then the tiger is rough.
((("rabbit" "eats" "tiger" "+")) -> ("tiger" "is" "rough" "+"))
If someone needs the tiger and they eat the cow then they need the rabbit.
((("someone" "needs" "tiger" "+") ("someone" "eats" "cow" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone visits the cat then they eat the cow.
((("someone" "visits" "cat" "+")) -> ("someone" "eats" "cow" "+"))
All cold people are rough.
((("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
If someone is red then they are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If someone is rough then they visit the tiger.
((("someone" "is" "rough" "+")) -> ("someone" "visits" "tiger" "+"))
If someone visits the rabbit then the rabbit is rough.
((("someone" "visits" "rabbit" "+")) -> ("rabbit" "is" "rough" "+"))
If someone needs the rabbit and the rabbit is red then they eat the cat.
((("someone" "needs" "rabbit" "+") ("rabbit" "is" "red" "+")) -> ("someone" "eats" "cat" "+"))
The rabbit eats the tiger.
True
1
proof
[(triple3)]
("rabbit" "eats" "tiger" "+")
triple3
The rabbit does not eat the tiger.
False
1
inv-proof
[(triple3)]
("rabbit" "eats" "tiger" "-")
triple3
The tiger is rough.
True
2
proof
[(((triple3) -> rule1))]
("tiger" "is" "rough" "+")
((triple3) -> (rule1 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The cow is not cold.
False
2
inv-proof
[(((triple2) -> rule5))]
("cow" "is" "cold" "-")
((triple2) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is rough.
True
3
proof
[(((((triple2) -> rule5)) -> rule4))]
("cow" "is" "rough" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The tiger does not visit the tiger.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule6))]
("tiger" "visits" "tiger" "-")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The cow visits the tiger.
True
4
proof
[(((((((triple2) -> rule5)) -> rule4)) -> rule6))]
("cow" "visits" "tiger" "+")
((((((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow does not visit the tiger.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule4)) -> rule6))]
("cow" "visits" "tiger" "-")
((((((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The tiger does not need the rabbit.
Unknown
inv-rconc
[@1: The tiger needs the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "needs" "rabbit" "-")
The rabbit needs the rabbit.
Unknown
rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "needs" "rabbit" "+")
The cat is not rough.
Unknown
inv-rconc
[@2: The cat is rough.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("cat" "is" "rough" "-")
The cow needs the rabbit.
Unknown
rconc
[@1: The cow needs the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "needs" "rabbit" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The cat eats the rabbit.
Unknown
random
[@0: The cat eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "rabbit" "+")
@0: The cat eats the cow.[(triple1)] The cow is red.[(triple2)] The rabbit eats the tiger.[(triple3)] The tiger needs the cat.[(triple4)] @1: The cow is cold.[(((triple2) -> rule5))] The tiger is rough.[(((triple3) -> rule1))] @2: The cow is rough.[(((((triple2) -> rule5)) -> rule4))] The tiger visits the tiger.[(((((triple3) -> rule1)) -> rule6))] @3: The cow visits the tiger.[(((((((triple2) -> rule5)) -> rule4)) -> rule6))]
The cat eats the cow.
("cat" "eats" "cow" "+")
triple1
The cow is red.
("cow" "is" "red" "+")
triple2
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple3
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple4
The cow is cold.
("cow" "is" "cold" "+")
((triple2) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
((triple3) -> (rule1 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The cow visits the tiger.
("cow" "visits" "tiger" "+")
((((((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3