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