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