The cat is blue. The cat is red. The cat needs the mouse. The cat sees the cow. The cat sees the mouse. The cow is big. The cow is red. The cow is young. The cow needs the mouse. The dog chases the cat. The dog is rough. The dog needs the mouse. The dog sees the cat. The dog sees the mouse. The mouse chases the cat. If someone sees the cow then they see the cat. If someone sees the cat then they are young. If the cow sees the dog and the cow needs the mouse then the cow needs the cat.
The cat is blue.
("cat" "is" "blue" "+")
The cat is red.
("cat" "is" "red" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is young.
("cow" "is" "young" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The dog chases the cat.
("dog" "chases" "cat" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
If someone sees the cow then they see the cat.
((("someone" "sees" "cow" "+")) -> ("someone" "sees" "cat" "+"))
If someone sees the cat then they are young.
((("someone" "sees" "cat" "+")) -> ("someone" "is" "young" "+"))
If the cow sees the dog and the cow needs the mouse then the cow needs the cat.
((("cow" "sees" "dog" "+") ("cow" "needs" "mouse" "+")) -> ("cow" "needs" "cat" "+"))
The cat is blue.
True
1
proof
[(triple1)]
("cat" "is" "blue" "+")
triple1
The dog does not see the mouse.
False
1
inv-proof
[(triple14)]
("dog" "sees" "mouse" "-")
triple14
The cat sees the cat.
True
2
proof
[(((triple4) -> rule1))]
("cat" "sees" "cat" "+")
((triple4) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat does not see the cat.
False
2
inv-proof
[(((triple4) -> rule1))]
("cat" "sees" "cat" "-")
((triple4) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is young.
True
3
proof
[(((((triple4) -> rule1)) -> rule2))]
("cat" "is" "young" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat is not young.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule2))]
("cat" "is" "young" "-")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cow does not see the cat.
Unknown
inv-rconc
[@1: The cow sees the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "sees" "cat" "-")
The mouse is young.
Unknown
rconc
[@2: The mouse is young.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("mouse" "is" "young" "+")
The cow does not need the cat.
Unknown
inv-rconc
[@1: The cow needs the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "needs" "cat" "-")
The mouse sees the dog.
Unknown
random
[@0: The mouse sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "dog" "+")
The dog does not need the cow.
Unknown
inv-random
[@0: The dog needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "cow" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
@0: The cat is blue.[(triple1)] The cat is red.[(triple2)] The cat needs the mouse.[(triple3)] The cat sees the cow.[(triple4)] The cat sees the mouse.[(triple5)] The cow is big.[(triple6)] The cow is red.[(triple7)] The cow is young.[(triple8)] The cow needs the mouse.[(triple9)] The dog chases the cat.[(triple10)] The dog is rough.[(triple11)] The dog needs the mouse.[(triple12)] The dog sees the cat.[(triple13)] The dog sees the mouse.[(triple14)] The mouse chases the cat.[(triple15)] @1: The cat sees the cat.[(((triple4) -> rule1))] The dog is young.[(((triple13) -> rule2))] @2: The cat is young.[(((((triple4) -> rule1)) -> rule2))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat is red.
("cat" "is" "red" "+")
triple2
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple3
The cat sees the cow.
("cat" "sees" "cow" "+")
triple4
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple5
The cow is big.
("cow" "is" "big" "+")
triple6
The cow is red.
("cow" "is" "red" "+")
triple7
The cow is young.
("cow" "is" "young" "+")
triple8
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple9
The dog chases the cat.
("dog" "chases" "cat" "+")
triple10
The dog is rough.
("dog" "is" "rough" "+")
triple11
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple12
The dog sees the cat.
("dog" "sees" "cat" "+")
triple13
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple14
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple15
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple4) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The dog is young.
("dog" "is" "young" "+")
((triple13) -> (rule2 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The cat is young.
("cat" "is" "young" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2