The cat chases the tiger. The cat is nice. The cat is round. The rabbit chases the cat. The rabbit is rough. The rabbit is round. The rabbit visits the tiger. The tiger eats the rabbit. The tiger is round. The tiger visits the cat. If someone is round and green then they eat the rabbit. Round people are rough. If the tiger eats the rabbit and the rabbit chases the tiger then the tiger visits the rabbit. If someone eats the tiger then they are round. Rough people are green. If someone visits the tiger and they are green then the tiger visits the rabbit.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is round.
("cat" "is" "round" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If someone is round and green then they eat the rabbit.
((("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "eats" "rabbit" "+"))
Round people are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
If the tiger eats the rabbit and the rabbit chases the tiger then the tiger visits the rabbit.
((("tiger" "eats" "rabbit" "+") ("rabbit" "chases" "tiger" "+")) -> ("tiger" "visits" "rabbit" "+"))
If someone eats the tiger then they are round.
((("someone" "eats" "tiger" "+")) -> ("someone" "is" "round" "+"))
Rough people are green.
((("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
If someone visits the tiger and they are green then the tiger visits the rabbit.
((("someone" "visits" "tiger" "+") ("someone" "is" "green" "+")) -> ("tiger" "visits" "rabbit" "+"))
The cat is nice.
True
1
proof
[(triple2)]
("cat" "is" "nice" "+")
triple2
The rabbit is not rough.
False
1
inv-proof
[(triple5 OR ((triple6) -> rule2))]
("rabbit" "is" "rough" "-")
triple5
((triple6) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The tiger is rough.
True
2
proof
[(((triple9) -> rule2))]
("tiger" "is" "rough" "+")
((triple9) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The rabbit is not green.
False
2
inv-proof
[(((triple5) -> rule5) OR ((((triple6) -> rule2)) -> rule5))]
("rabbit" "is" "green" "-")
((triple5) -> (rule5 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The tiger visits the rabbit.
True
4
proof
[(((triple7 ((triple5) -> rule5)) -> rule6) OR ((triple7 ((((triple6) -> rule2)) -> rule5)) -> rule6))]
("tiger" "visits" "rabbit" "+")
((triple7 ((triple5) -> (rule5 % int2))) -> (rule6 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
((triple7 ((((triple6) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
int3
The tiger does not visit the rabbit.
False
4
inv-proof
[(((triple7 ((triple5) -> rule5)) -> rule6) OR ((triple7 ((((triple6) -> rule2)) -> rule5)) -> rule6))]
("tiger" "visits" "rabbit" "-")
((triple7 ((triple5) -> (rule5 % int2))) -> (rule6 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
((triple7 ((((triple6) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
int3
The cat eats the rabbit.
True
5
proof
[(((triple3 ((((triple3) -> rule2)) -> rule5)) -> rule1))]
("cat" "eats" "rabbit" "+")
((triple3 ((((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The cat does not eat the rabbit.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule2)) -> rule5)) -> rule1))]
("cat" "eats" "rabbit" "-")
((triple3 ((((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
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 rabbit visits the cat.
Unknown
random
[@0: The rabbit visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "cat" "+")
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
The rabbit does not chase the tiger.
Unknown
inv-random
[@0: The rabbit chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "tiger" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
The rabbit is not nice.
Unknown
inv-random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "-")
The tiger chases the cat.
Unknown
random
[@0: The tiger chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "cat" "+")
@0: The cat chases the tiger.[(triple1)] The cat is nice.[(triple2)] The cat is round.[(triple3)] The rabbit chases the cat.[(triple4)] The rabbit is rough.[(triple5 OR ((triple6) -> rule2))] The rabbit is round.[(triple6)] The rabbit visits the tiger.[(triple7)] The tiger eats the rabbit.[(triple8 OR ((triple9 ((((triple9) -> rule2)) -> rule5)) -> rule1))] The tiger is round.[(triple9)] The tiger visits the cat.[(triple10)] @1: The cat is rough.[(((triple3) -> rule2))] The rabbit is green.[(((triple5) -> rule5) OR ((((triple6) -> rule2)) -> rule5))] The tiger is rough.[(((triple9) -> rule2))] @2: The cat is green.[(((((triple3) -> rule2)) -> rule5))] The rabbit eats the rabbit.[(((triple6 ((triple5) -> rule5)) -> rule1) OR ((triple6 ((((triple6) -> rule2)) -> rule5)) -> rule1))] The tiger is green.[(((((triple9) -> rule2)) -> rule5))] The tiger visits the rabbit.[(((triple7 ((triple5) -> rule5)) -> rule6) OR ((triple7 ((((triple6) -> rule2)) -> rule5)) -> rule6))] @3: The cat eats the rabbit.[(((triple3 ((((triple3) -> rule2)) -> rule5)) -> rule1))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat is round.
("cat" "is" "round" "+")
triple3
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple4
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple5
((triple6) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
triple6
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple7
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple8
((triple9 ((((triple9) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is rough.
("tiger" "is" "rough" "+")
int3
The tiger is round.
("tiger" "is" "round" "+")
triple9
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple10
The cat is rough.
("cat" "is" "rough" "+")
((triple3) -> (rule2 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
((triple5) -> (rule5 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The tiger is rough.
("tiger" "is" "rough" "+")
((triple9) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The cat is green.
("cat" "is" "green" "+")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((triple6 ((triple5) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
((triple6 ((((triple6) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
int3
The tiger is green.
("tiger" "is" "green" "+")
((((triple9) -> (rule2 % int2))) -> (rule5 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
((triple7 ((triple5) -> (rule5 % int2))) -> (rule6 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
((triple7 ((((triple6) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
int3
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
((triple3 ((((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3