The cat is green. The cat is red. The cat is rough. The cat does not need the rabbit. The cat sees the rabbit. The rabbit does not chase the cat. The rabbit is not big. The rabbit is green. The rabbit is red. The rabbit is rough. The rabbit does not need the cat. The rabbit does not see the cat. If the rabbit is not green then the rabbit does not chase the cat. If someone is cold then they chase the rabbit. If someone sees the cat then they do not chase the rabbit. If someone needs the rabbit then they are cold. If someone needs the rabbit then they see the cat. If someone sees the rabbit then they see the cat.
The cat is green.
("cat" "is" "green" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat does not need the rabbit.
("cat" "needs" "rabbit" "-")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
The rabbit is not big.
("rabbit" "is" "big" "-")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit does not need the cat.
("rabbit" "needs" "cat" "-")
The rabbit does not see the cat.
("rabbit" "sees" "cat" "-")
If the rabbit is not green then the rabbit does not chase the cat.
((("rabbit" "is" "green" "~")) -> ("rabbit" "chases" "cat" "-"))
If someone is cold then they chase the rabbit.
((("someone" "is" "cold" "+")) -> ("someone" "chases" "rabbit" "+"))
If someone sees the cat then they do not chase the rabbit.
((("someone" "sees" "cat" "+")) -> ("someone" "chases" "rabbit" "-"))
If someone needs the rabbit then they are cold.
((("someone" "needs" "rabbit" "+")) -> ("someone" "is" "cold" "+"))
If someone needs the rabbit then they see the cat.
((("someone" "needs" "rabbit" "+")) -> ("someone" "sees" "cat" "+"))
If someone sees the rabbit then they see the cat.
((("someone" "sees" "rabbit" "+")) -> ("someone" "sees" "cat" "+"))
The rabbit is green.
True
1
proof
[(triple8)]
("rabbit" "is" "green" "+")
triple8
The cat is not rough.
False
1
inv-proof
[(triple3)]
("cat" "is" "rough" "-")
triple3
The cat sees the cat.
True
2
proof
[(((triple5) -> rule6))]
("cat" "sees" "cat" "+")
((triple5) -> (rule6 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat does not see the cat.
False
2
inv-proof
[(((triple5) -> rule6))]
("cat" "sees" "cat" "-")
((triple5) -> (rule6 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat does not chase the rabbit.
True
3
proof
[(((((triple5) -> rule6)) -> rule3))]
("cat" "chases" "rabbit" "-")
((((triple5) -> (rule6 % int2))) -> (rule3 % int1))
The cat does not chase the rabbit.
("cat" "chases" "rabbit" "-")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat chases the rabbit.
False
3
inv-proof
[(((((triple5) -> rule6)) -> rule3))]
("cat" "chases" "rabbit" "+")
((((triple5) -> (rule6 % int2))) -> (rule3 % int1))
The cat does not chase the rabbit.
("cat" "chases" "rabbit" "-")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The rabbit does not chase the rabbit.
Unknown
inv-rconc
[@2: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("rabbit" "chases" "rabbit" "-")
The rabbit is cold.
Unknown
rconc
[@1: The rabbit is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "is" "cold" "+")
The cat is not cold.
Unknown
inv-rconc
[@1: The cat is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "cold" "-")
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 need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
@0: The cat does not need the rabbit.[(triple4)] The cat is green.[(triple1)] The cat is red.[(triple2)] The cat is rough.[(triple3)] The cat sees the rabbit.[(triple5)] The rabbit does not chase the cat.[(triple6)] The rabbit does not need the cat.[(triple11)] The rabbit does not see the cat.[(triple12)] The rabbit is green.[(triple8)] The rabbit is not big.[(triple7)] The rabbit is red.[(triple9)] The rabbit is rough.[(triple10)] @1: The cat sees the cat.[(((triple5) -> rule6))] @2: The cat does not chase the rabbit.[(((((triple5) -> rule6)) -> rule3))]
The cat does not need the rabbit.
("cat" "needs" "rabbit" "-")
triple4
The cat is green.
("cat" "is" "green" "+")
triple1
The cat is red.
("cat" "is" "red" "+")
triple2
The cat is rough.
("cat" "is" "rough" "+")
triple3
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple5
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
triple6
The rabbit does not need the cat.
("rabbit" "needs" "cat" "-")
triple11
The rabbit does not see the cat.
("rabbit" "sees" "cat" "-")
triple12
The rabbit is green.
("rabbit" "is" "green" "+")
triple8
The rabbit is not big.
("rabbit" "is" "big" "-")
triple7
The rabbit is red.
("rabbit" "is" "red" "+")
triple9
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple10
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple5) -> (rule6 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat does not chase the rabbit.
("cat" "chases" "rabbit" "-")
((((triple5) -> (rule6 % int2))) -> (rule3 % int1))
The cat does not chase the rabbit.
("cat" "chases" "rabbit" "-")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2