The cat visits the rabbit. The rabbit is cold. The rabbit is green. The rabbit needs the cat. The rabbit needs the tiger. The tiger needs the rabbit. The tiger visits the cat. If someone is green then they visit the cat. If someone is green and they visit the cat then the cat eats the rabbit. If someone eats the rabbit then the rabbit is rough.
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If someone is green then they visit the cat.
((("someone" "is" "green" "+")) -> ("someone" "visits" "cat" "+"))
If someone is green and they visit the cat then the cat eats the rabbit.
((("someone" "is" "green" "+") ("someone" "visits" "cat" "+")) -> ("cat" "eats" "rabbit" "+"))
If someone eats the rabbit then the rabbit is rough.
((("someone" "eats" "rabbit" "+")) -> ("rabbit" "is" "rough" "+"))
The rabbit is green.
True
1
proof
[(triple3)]
("rabbit" "is" "green" "+")
triple3
The rabbit is not cold.
False
1
inv-proof
[(triple2)]
("rabbit" "is" "cold" "-")
triple2
The rabbit visits the cat.
True
2
proof
[(((triple3) -> rule1))]
("rabbit" "visits" "cat" "+")
((triple3) -> (rule1 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The rabbit does not visit the cat.
False
2
inv-proof
[(((triple3) -> rule1))]
("rabbit" "visits" "cat" "-")
((triple3) -> (rule1 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The cat eats the rabbit.
True
4
proof
[(((triple3 ((triple3) -> rule1)) -> rule2))]
("cat" "eats" "rabbit" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The cat does not eat the rabbit.
False
4
inv-proof
[(((triple3 ((triple3) -> rule1)) -> rule2))]
("cat" "eats" "rabbit" "-")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The rabbit is rough.
True
5
proof
[(((((triple3 ((triple3) -> rule1)) -> rule2)) -> rule3))]
("rabbit" "is" "rough" "+")
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int2
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int3
The rabbit is not rough.
False
5
inv-proof
[(((((triple3 ((triple3) -> rule1)) -> rule2)) -> rule3))]
("rabbit" "is" "rough" "-")
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int2
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int3
The cat does not visit the cat.
Unknown
inv-rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "visits" "cat" "-")
The tiger eats the rabbit.
Unknown
random
[@0: The tiger eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "rabbit" "+")
The tiger is not green.
Unknown
inv-random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
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 is cold.
Unknown
random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "+")
@0: The cat visits the rabbit.[(triple1)] The rabbit is cold.[(triple2)] The rabbit is green.[(triple3)] The rabbit needs the cat.[(triple4)] The rabbit needs the tiger.[(triple5)] The tiger needs the rabbit.[(triple6)] The tiger visits the cat.[(triple7)] @1: The rabbit visits the cat.[(((triple3) -> rule1))] @2: The cat eats the rabbit.[(((triple3 ((triple3) -> rule1)) -> rule2))] @3: The rabbit is rough.[(((((triple3 ((triple3) -> rule1)) -> rule2)) -> rule3))]
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple1
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple2
The rabbit is green.
("rabbit" "is" "green" "+")
triple3
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple4
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple5
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple6
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple7
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
((triple3) -> (rule1 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int2
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int3