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