The cat is rough. The rabbit eats the cat. The rabbit is big. The rabbit is red. The rabbit is rough. The rabbit is young. The rabbit visits the cat. If someone eats the cat then the cat eats the rabbit. If someone visits the cat then the cat needs the rabbit. If someone is young then they visit the rabbit. If someone is rough then they are young. If someone needs the rabbit then they visit the cat. If the rabbit needs the cat then the cat visits the rabbit. Big people are young. If someone is young then they eat the cat.
The cat is rough.
("cat" "is" "rough" "+")
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
If someone eats the cat then the cat eats the rabbit.
((("someone" "eats" "cat" "+")) -> ("cat" "eats" "rabbit" "+"))
If someone visits the cat then the cat needs the rabbit.
((("someone" "visits" "cat" "+")) -> ("cat" "needs" "rabbit" "+"))
If someone is young then they visit the rabbit.
((("someone" "is" "young" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone is rough then they are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If someone needs the rabbit then they visit the cat.
((("someone" "needs" "rabbit" "+")) -> ("someone" "visits" "cat" "+"))
If the rabbit needs the cat then the cat visits the rabbit.
((("rabbit" "needs" "cat" "+")) -> ("cat" "visits" "rabbit" "+"))
Big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If someone is young then they eat the cat.
((("someone" "is" "young" "+")) -> ("someone" "eats" "cat" "+"))
The rabbit is big.
True
1
proof
[(triple3)]
("rabbit" "is" "big" "+")
triple3
The rabbit does not visit the cat.
False
1
inv-proof
[(triple7)]
("rabbit" "visits" "cat" "-")
triple7
The rabbit does not eat the rabbit.
Unknown
inv-random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
@0: The cat is rough.[(triple1)] The rabbit eats the cat.[(triple2 OR ((triple6) -> rule8) OR ((((triple3) -> rule7)) -> rule8) OR ((((triple5) -> rule4)) -> rule8))] The rabbit is big.[(triple3)] The rabbit is red.[(triple4)] The rabbit is rough.[(triple5)] The rabbit is young.[(triple6 OR ((triple3) -> rule7) OR ((triple5) -> rule4))] The rabbit visits the cat.[(triple7)] @1: The cat eats the rabbit.[(((triple2) -> rule1) OR ((((triple6) -> rule8)) -> rule1) OR ((((((triple1) -> rule4)) -> rule8)) -> rule1) OR ((((((triple3) -> rule7)) -> rule8)) -> rule1) OR ((((((triple5) -> rule4)) -> rule8)) -> rule1))] The cat is young.[(((triple1) -> rule4))] The cat needs the rabbit.[(((triple7) -> rule2))] The rabbit visits the rabbit.[(((triple6) -> rule3) OR ((((triple3) -> rule7)) -> rule3) OR ((((triple5) -> rule4)) -> rule3))] @2: The cat eats the cat.[(((((triple1) -> rule4)) -> rule8))] The cat visits the cat.[(((((triple7) -> rule2)) -> rule5))] The cat visits the rabbit.[(((((triple1) -> rule4)) -> rule3))]
The cat is rough.
("cat" "is" "rough" "+")
triple1
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple2
((triple6) -> (rule8 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule8 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
((((triple5) -> (rule4 % int2))) -> (rule8 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
triple3
The rabbit is red.
("rabbit" "is" "red" "+")
triple4
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple5
The rabbit is young.
("rabbit" "is" "young" "+")
triple6
((triple3) -> (rule7 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
((triple5) -> (rule4 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple7
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
((triple2) -> (rule1 % int1))
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int1
((((triple6) -> (rule8 % int2))) -> (rule1 % int1))
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int1
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2
The cat is young.
("cat" "is" "young" "+")
int3
((((((triple3) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int1
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
int3
((((((triple5) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int1
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
int3
The cat is young.
("cat" "is" "young" "+")
((triple1) -> (rule4 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
((triple7) -> (rule2 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple6) -> (rule3 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
((((triple5) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
((((triple1) -> (rule4 % int2))) -> (rule8 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat visits the cat.
("cat" "visits" "cat" "+")
((((triple7) -> (rule2 % int2))) -> (rule5 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int2
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2