The cat is round. The cat is young. The cat likes the dog. The cat likes the mouse. The cat needs the dog. The cat sees the dog. The dog is blue. The dog is red. The dog likes the cat. The dog likes the mouse. The dog needs the mouse. The dog sees the cat. The dog sees the mouse. The mouse is big. The mouse likes the cat. If something likes the cat then it sees the cat. If something likes the mouse and the mouse sees the cat then it is big. If something sees the mouse then the mouse is young. If something likes the dog and the dog needs the cat then the dog likes the cat. If something is round and big then it sees the cat. If something is young and it needs the mouse then the mouse sees the cat.
The cat is round.
("cat" "is" "round" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the dog.
("cat" "likes" "dog" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The cat sees the dog.
("cat" "sees" "dog" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is red.
("dog" "is" "red" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
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 is big.
("mouse" "is" "big" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
If something likes the cat then it sees the cat.
((("something" "likes" "cat" "+")) -> ("something" "sees" "cat" "+"))
If something likes the mouse and the mouse sees the cat then it is big.
((("something" "likes" "mouse" "+") ("mouse" "sees" "cat" "+")) -> ("something" "is" "big" "+"))
If something sees the mouse then the mouse is young.
((("something" "sees" "mouse" "+")) -> ("mouse" "is" "young" "+"))
If something likes the dog and the dog needs the cat then the dog likes the cat.
((("something" "likes" "dog" "+") ("dog" "needs" "cat" "+")) -> ("dog" "likes" "cat" "+"))
If something is round and big then it sees the cat.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "sees" "cat" "+"))
If something is young and it needs the mouse then the mouse sees the cat.
((("something" "is" "young" "+") ("something" "needs" "mouse" "+")) -> ("mouse" "sees" "cat" "+"))
The dog likes the cat.
True
1
proof
[(triple9)]
("dog" "likes" "cat" "+")
triple9
The dog does not need the mouse.
False
1
inv-proof
[(triple11)]
("dog" "needs" "mouse" "-")
triple11
The mouse sees the cat.
True
2
proof
[(((triple15) -> rule1))]
("mouse" "sees" "cat" "+")
((triple15) -> (rule1 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The mouse is not young.
False
2
inv-proof
[(((triple13) -> rule3))]
("mouse" "is" "young" "-")
((triple13) -> (rule3 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The dog is big.
True
4
proof
[(((triple10 ((triple15) -> rule1)) -> rule2))]
("dog" "is" "big" "+")
((triple10 ((triple15) -> (rule1 % int2))) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The cat is not big.
False
4
inv-proof
[(((triple4 ((triple15) -> rule1)) -> rule2))]
("cat" "is" "big" "-")
((triple4 ((triple15) -> (rule1 % int2))) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The cat sees the cat.
True
6
proof
[(((triple1 ((triple4 ((triple15) -> rule1)) -> rule2)) -> rule5))]
("cat" "sees" "cat" "+")
((triple1 ((triple4 ((triple15) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int3
The cat does not see the cat.
False
6
inv-proof
[(((triple1 ((triple4 ((triple15) -> rule1)) -> rule2)) -> rule5))]
("cat" "sees" "cat" "-")
((triple1 ((triple4 ((triple15) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int3
The dog does not need the cat.
Unknown
inv-random
[@0: The dog needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "cat" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
The dog does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The cat is blue.
Unknown
random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The cat is red.
Unknown
random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "+")
The mouse is not round.
Unknown
inv-random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "-")
The dog is young.
Unknown
random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "+")
@0: The cat is round.[(triple1)] The cat is young.[(triple2)] The cat likes the dog.[(triple3)] The cat likes the mouse.[(triple4)] The cat needs the dog.[(triple5)] The cat sees the dog.[(triple6)] The dog is blue.[(triple7)] The dog is red.[(triple8)] The dog likes the cat.[(triple9)] The dog likes the mouse.[(triple10)] The dog needs the mouse.[(triple11)] The dog sees the cat.[(triple12 OR ((triple9) -> rule1))] The dog sees the mouse.[(triple13)] The mouse is big.[(triple14)] The mouse likes the cat.[(triple15)] @1: The mouse is young.[(((triple13) -> rule3))] The mouse sees the cat.[(((triple15) -> rule1))] @2: The cat is big.[(((triple4 ((triple15) -> rule1)) -> rule2))] The dog is big.[(((triple10 ((triple15) -> rule1)) -> rule2))] @3: The cat sees the cat.[(((triple1 ((triple4 ((triple15) -> rule1)) -> rule2)) -> rule5))]
The cat is round.
("cat" "is" "round" "+")
triple1
The cat is young.
("cat" "is" "young" "+")
triple2
The cat likes the dog.
("cat" "likes" "dog" "+")
triple3
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple4
The cat needs the dog.
("cat" "needs" "dog" "+")
triple5
The cat sees the dog.
("cat" "sees" "dog" "+")
triple6
The dog is blue.
("dog" "is" "blue" "+")
triple7
The dog is red.
("dog" "is" "red" "+")
triple8
The dog likes the cat.
("dog" "likes" "cat" "+")
triple9
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple10
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple11
The dog sees the cat.
("dog" "sees" "cat" "+")
triple12
((triple9) -> (rule1 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple13
The mouse is big.
("mouse" "is" "big" "+")
triple14
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple15
The mouse is young.
("mouse" "is" "young" "+")
((triple13) -> (rule3 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
((triple15) -> (rule1 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The cat is big.
("cat" "is" "big" "+")
((triple4 ((triple15) -> (rule1 % int2))) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The dog is big.
("dog" "is" "big" "+")
((triple10 ((triple15) -> (rule1 % int2))) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple1 ((triple4 ((triple15) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int3