The cat is blue. The cat sees the tiger. The dog sees the tiger. The squirrel chases the cat. The squirrel is big. The tiger chases the squirrel. The tiger sees the dog. If something sees the squirrel and the squirrel sees the tiger then it sees the dog. All big things are blue. If something is blue and it chases the cat then the cat likes the dog.
The cat is blue.
("cat" "is" "blue" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
If something sees the squirrel and the squirrel sees the tiger then it sees the dog.
((("something" "sees" "squirrel" "+") ("squirrel" "sees" "tiger" "+")) -> ("something" "sees" "dog" "+"))
All big things are blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If something is blue and it chases the cat then the cat likes the dog.
((("something" "is" "blue" "+") ("something" "chases" "cat" "+")) -> ("cat" "likes" "dog" "+"))
The tiger chases the squirrel.
True
1
proof
[(triple6)]
("tiger" "chases" "squirrel" "+")
triple6
The dog does not see the tiger.
False
1
inv-proof
[(triple3)]
("dog" "sees" "tiger" "-")
triple3
The squirrel is blue.
True
2
proof
[(((triple5) -> rule2))]
("squirrel" "is" "blue" "+")
((triple5) -> (rule2 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is not blue.
False
2
inv-proof
[(((triple5) -> rule2))]
("squirrel" "is" "blue" "-")
((triple5) -> (rule2 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The cat likes the dog.
True
4
proof
[(((((triple5) -> rule2) triple4) -> rule3))]
("cat" "likes" "dog" "+")
((((triple5) -> (rule2 % int2)) triple4) -> (rule3 % int1))
The cat likes the dog.
("cat" "likes" "dog" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The cat does not like the dog.
False
4
inv-proof
[(((((triple5) -> rule2) triple4) -> rule3))]
("cat" "likes" "dog" "-")
((((triple5) -> (rule2 % int2)) triple4) -> (rule3 % int1))
The cat likes the dog.
("cat" "likes" "dog" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The tiger is not blue.
Unknown
inv-rconc
[@1: The tiger is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "blue" "-")
The dog sees the dog.
Unknown
rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "sees" "dog" "+")
The dog is not blue.
Unknown
inv-rconc
[@1: The dog is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "blue" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The cat is not round.
Unknown
inv-random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The cat is blue.[(triple1)] The cat sees the tiger.[(triple2)] The dog sees the tiger.[(triple3)] The squirrel chases the cat.[(triple4)] The squirrel is big.[(triple5)] The tiger chases the squirrel.[(triple6)] The tiger sees the dog.[(triple7)] @1: The squirrel is blue.[(((triple5) -> rule2))] @2: The cat likes the dog.[(((((triple5) -> rule2) triple4) -> rule3))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple2
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple3
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
triple4
The squirrel is big.
("squirrel" "is" "big" "+")
triple5
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple6
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple7
The squirrel is blue.
("squirrel" "is" "blue" "+")
((triple5) -> (rule2 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The cat likes the dog.
("cat" "likes" "dog" "+")
((((triple5) -> (rule2 % int2)) triple4) -> (rule3 % int1))
The cat likes the dog.
("cat" "likes" "dog" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2