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