The cat is green. The cat sees the dog. The cat sees the rabbit. The cat visits the rabbit. The dog needs the cat. The dog does not need the squirrel. The dog does not see the rabbit. The rabbit is blue. The rabbit is green. The rabbit needs the squirrel. The rabbit does not see the cat. The rabbit sees the squirrel. The rabbit visits the squirrel. The squirrel needs the rabbit. The squirrel does not visit the rabbit. Kind things are not big. If something sees the cat then the cat is green. If something visits the rabbit then the rabbit is kind.
The cat is green.
("cat" "is" "green" "+")
The cat sees the dog.
("cat" "sees" "dog" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The dog does not need the squirrel.
("dog" "needs" "squirrel" "-")
The dog does not see the rabbit.
("dog" "sees" "rabbit" "-")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
The rabbit does not see the cat.
("rabbit" "sees" "cat" "-")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
The squirrel does not visit the rabbit.
("squirrel" "visits" "rabbit" "-")
Kind things are not big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "-"))
If something sees the cat then the cat is green.
((("something" "sees" "cat" "+")) -> ("cat" "is" "green" "+"))
If something visits the rabbit then the rabbit is kind.
((("something" "visits" "rabbit" "+")) -> ("rabbit" "is" "kind" "+"))
The dog does not see the rabbit.
True
1
proof
[(triple7)]
("dog" "sees" "rabbit" "-")
triple7
The squirrel visits the rabbit.
False
1
inv-proof
[(triple15)]
("squirrel" "visits" "rabbit" "+")
triple15
The rabbit is kind.
True
2
proof
[(((triple4) -> rule3))]
("rabbit" "is" "kind" "+")
((triple4) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is not kind.
False
2
inv-proof
[(((triple4) -> rule3))]
("rabbit" "is" "kind" "-")
((triple4) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is not big.
True
3
proof
[(((((triple4) -> rule3)) -> rule1))]
("rabbit" "is" "big" "-")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit is not big.
("rabbit" "is" "big" "-")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit is big.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule1))]
("rabbit" "is" "big" "+")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit is not big.
("rabbit" "is" "big" "-")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The squirrel does not see the squirrel.
Unknown
inv-random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
The squirrel does not need the cat.
Unknown
inv-random
[@0: The squirrel needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "cat" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
The cat does not see the squirrel.
Unknown
inv-random
[@0: The cat sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "squirrel" "-")
The rabbit sees the dog.
Unknown
random
[@0: The rabbit sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "dog" "+")
@0: The cat is green.[(triple1)] The cat sees the dog.[(triple2)] The cat sees the rabbit.[(triple3)] The cat visits the rabbit.[(triple4)] The dog does not need the squirrel.[(triple6)] The dog does not see the rabbit.[(triple7)] The dog needs the cat.[(triple5)] The rabbit does not see the cat.[(triple11)] The rabbit is blue.[(triple8)] The rabbit is green.[(triple9)] The rabbit needs the squirrel.[(triple10)] The rabbit sees the squirrel.[(triple12)] The rabbit visits the squirrel.[(triple13)] The squirrel does not visit the rabbit.[(triple15)] The squirrel needs the rabbit.[(triple14)] @1: The rabbit is kind.[(((triple4) -> rule3))] @2: The rabbit is not big.[(((((triple4) -> rule3)) -> rule1))]
The cat is green.
("cat" "is" "green" "+")
triple1
The cat sees the dog.
("cat" "sees" "dog" "+")
triple2
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple3
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple4
The dog does not need the squirrel.
("dog" "needs" "squirrel" "-")
triple6
The dog does not see the rabbit.
("dog" "sees" "rabbit" "-")
triple7
The dog needs the cat.
("dog" "needs" "cat" "+")
triple5
The rabbit does not see the cat.
("rabbit" "sees" "cat" "-")
triple11
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple8
The rabbit is green.
("rabbit" "is" "green" "+")
triple9
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
triple10
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple12
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple13
The squirrel does not visit the rabbit.
("squirrel" "visits" "rabbit" "-")
triple15
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple14
The rabbit is kind.
("rabbit" "is" "kind" "+")
((triple4) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is not big.
("rabbit" "is" "big" "-")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit is not big.
("rabbit" "is" "big" "-")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2