The cat chases the rabbit. The cat eats the rabbit. The cat is cold. The cat is kind. The cat is nice. The cat sees the rabbit. The rabbit chases the cat. The rabbit eats the cat. The rabbit is cold. The rabbit is nice. The rabbit is young. The rabbit sees the cat. If someone sees the cat and they eat the cat then the cat is rough. If someone eats the rabbit then they eat the cat. If someone chases the rabbit then they chase the cat. If someone sees the cat and the cat eats the rabbit then the cat chases the rabbit. If someone is kind and cold then they see the rabbit. If someone chases the cat and they are young then they see the rabbit. If someone chases the cat and the cat is kind then the cat sees the rabbit. If someone sees the cat then they chase the rabbit.
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
If someone sees the cat and they eat the cat then the cat is rough.
((("someone" "sees" "cat" "+") ("someone" "eats" "cat" "+")) -> ("cat" "is" "rough" "+"))
If someone eats the rabbit then they eat the cat.
((("someone" "eats" "rabbit" "+")) -> ("someone" "eats" "cat" "+"))
If someone chases the rabbit then they chase the cat.
((("someone" "chases" "rabbit" "+")) -> ("someone" "chases" "cat" "+"))
If someone sees the cat and the cat eats the rabbit then the cat chases the rabbit.
((("someone" "sees" "cat" "+") ("cat" "eats" "rabbit" "+")) -> ("cat" "chases" "rabbit" "+"))
If someone is kind and cold then they see the rabbit.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone chases the cat and they are young then they see the rabbit.
((("someone" "chases" "cat" "+") ("someone" "is" "young" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone chases the cat and the cat is kind then the cat sees the rabbit.
((("someone" "chases" "cat" "+") ("cat" "is" "kind" "+")) -> ("cat" "sees" "rabbit" "+"))
If someone sees the cat then they chase the rabbit.
((("someone" "sees" "cat" "+")) -> ("someone" "chases" "rabbit" "+"))
The rabbit is nice.
True
1
proof
[(triple10)]
("rabbit" "is" "nice" "+")
triple10
The cat does not eat the rabbit.
False
1
inv-proof
[(triple2)]
("cat" "eats" "rabbit" "-")
triple2
The rabbit sees the rabbit.
True
3
proof
[(((triple7 triple11) -> rule6) OR ((((((triple12) -> rule8)) -> rule3) triple11) -> rule6))]
("rabbit" "sees" "rabbit" "+")
((triple7 triple11) -> (rule6 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
((((((triple12) -> (rule8 % int3))) -> (rule3 % int2)) triple11) -> (rule6 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int3
The cat is not rough.
False
3
inv-proof
[(((triple12 triple8) -> rule1))]
("cat" "is" "rough" "-")
((triple12 triple8) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
The cat is not young.
Unknown
inv-random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
@0: The cat chases the rabbit.[(triple1 OR ((triple12 triple2) -> rule4))] The cat eats the rabbit.[(triple2)] The cat is cold.[(triple3)] The cat is kind.[(triple4)] The cat is nice.[(triple5)] The cat sees the rabbit.[(triple6 OR ((triple4 triple3) -> rule5) OR ((triple7 triple4) -> rule7) OR ((((triple1) -> rule3) triple4) -> rule7) OR ((((((triple12) -> rule8)) -> rule3) triple4) -> rule7) OR ((((((triple12 triple2) -> rule4)) -> rule3) triple4) -> rule7))] The rabbit chases the cat.[(triple7 OR ((((triple12) -> rule8)) -> rule3))] The rabbit eats the cat.[(triple8)] The rabbit is cold.[(triple9)] The rabbit is nice.[(triple10)] The rabbit is young.[(triple11)] The rabbit sees the cat.[(triple12)] @1: The cat chases the cat.[(((triple1) -> rule3) OR ((((triple12 triple2) -> rule4)) -> rule3))] The cat eats the cat.[(((triple2) -> rule2))] The cat is rough.[(((triple12 triple8) -> rule1))] The rabbit chases the rabbit.[(((triple12) -> rule8))] The rabbit sees the rabbit.[(((triple7 triple11) -> rule6) OR ((((((triple12) -> rule8)) -> rule3) triple11) -> rule6))]
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple1
((triple12 triple2) -> (rule4 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple2
The cat is cold.
("cat" "is" "cold" "+")
triple3
The cat is kind.
("cat" "is" "kind" "+")
triple4
The cat is nice.
("cat" "is" "nice" "+")
triple5
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple6
((triple4 triple3) -> (rule5 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
((triple7 triple4) -> (rule7 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
((((triple1) -> (rule3 % int2)) triple4) -> (rule7 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
((((((triple12) -> (rule8 % int3))) -> (rule3 % int2)) triple4) -> (rule7 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int3
((((((triple12 triple2) -> (rule4 % int3))) -> (rule3 % int2)) triple4) -> (rule7 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int3
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple7
((((triple12) -> (rule8 % int2))) -> (rule3 % int1))
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple8
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple9
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple10
The rabbit is young.
("rabbit" "is" "young" "+")
triple11
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple12
The cat chases the cat.
("cat" "chases" "cat" "+")
((triple1) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
((((triple12 triple2) -> (rule4 % int2))) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
((triple2) -> (rule2 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
((triple12 triple8) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple12) -> (rule8 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((triple7 triple11) -> (rule6 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
((((((triple12) -> (rule8 % int3))) -> (rule3 % int2)) triple11) -> (rule6 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int3