The dog is big. The dog likes the mouse. The dog likes the tiger. The dog sees the squirrel. The dog sees the tiger. The dog visits the mouse. The dog visits the squirrel. The mouse sees the squirrel. The mouse visits the squirrel. The mouse visits the tiger. The squirrel is big. The squirrel sees the tiger. The squirrel visits the tiger. The tiger is big. The tiger is young. The tiger sees the mouse. If something is round then it is blue. If the tiger sees the mouse then the mouse is big. If something is big then it is round.
The dog is big.
("dog" "is" "big" "+")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If something is round then it is blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If the tiger sees the mouse then the mouse is big.
((("tiger" "sees" "mouse" "+")) -> ("mouse" "is" "big" "+"))
If something is big then it is round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
The dog sees the squirrel.
True
1
proof
[(triple4)]
("dog" "sees" "squirrel" "+")
triple4
The dog is not big.
False
1
inv-proof
[(triple1)]
("dog" "is" "big" "-")
triple1
The squirrel is round.
True
2
proof
[(((triple11) -> rule3))]
("squirrel" "is" "round" "+")
((triple11) -> (rule3 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The mouse is not big.
False
2
inv-proof
[(((triple16) -> rule2))]
("mouse" "is" "big" "-")
((triple16) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The squirrel is blue.
True
3
proof
[(((((triple11) -> rule3)) -> rule1))]
("squirrel" "is" "blue" "+")
((((triple11) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The squirrel is not blue.
False
3
inv-proof
[(((((triple11) -> rule3)) -> rule1))]
("squirrel" "is" "blue" "-")
((((triple11) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The mouse is blue.
True
4
proof
[(((((((triple16) -> rule2)) -> rule3)) -> rule1))]
("mouse" "is" "blue" "+")
((((((triple16) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3
The mouse is not blue.
False
4
inv-proof
[(((((((triple16) -> rule2)) -> rule3)) -> rule1))]
("mouse" "is" "blue" "-")
((((((triple16) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
The squirrel does not like the tiger.
Unknown
inv-random
[@0: The squirrel likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "tiger" "-")
The dog is kind.
Unknown
random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "+")
The dog does not see the mouse.
Unknown
inv-random
[@0: The dog sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "mouse" "-")
The tiger visits the dog.
Unknown
random
[@0: The tiger visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "dog" "+")
The mouse does not like the dog.
Unknown
inv-random
[@0: The mouse likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "dog" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
@0: The dog is big.[(triple1)] The dog likes the mouse.[(triple2)] The dog likes the tiger.[(triple3)] The dog sees the squirrel.[(triple4)] The dog sees the tiger.[(triple5)] The dog visits the mouse.[(triple6)] The dog visits the squirrel.[(triple7)] The mouse sees the squirrel.[(triple8)] The mouse visits the squirrel.[(triple9)] The mouse visits the tiger.[(triple10)] The squirrel is big.[(triple11)] The squirrel sees the tiger.[(triple12)] The squirrel visits the tiger.[(triple13)] The tiger is big.[(triple14)] The tiger is young.[(triple15)] The tiger sees the mouse.[(triple16)] @1: The dog is round.[(((triple1) -> rule3))] The mouse is big.[(((triple16) -> rule2))] The squirrel is round.[(((triple11) -> rule3))] The tiger is round.[(((triple14) -> rule3))] @2: The dog is blue.[(((((triple1) -> rule3)) -> rule1))] The mouse is round.[(((((triple16) -> rule2)) -> rule3))] The squirrel is blue.[(((((triple11) -> rule3)) -> rule1))] The tiger is blue.[(((((triple14) -> rule3)) -> rule1))] @3: The mouse is blue.[(((((((triple16) -> rule2)) -> rule3)) -> rule1))]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple2
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple3
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple4
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple5
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple6
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
triple7
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple8
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple9
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple10
The squirrel is big.
("squirrel" "is" "big" "+")
triple11
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple12
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple13
The tiger is big.
("tiger" "is" "big" "+")
triple14
The tiger is young.
("tiger" "is" "young" "+")
triple15
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple16
The dog is round.
("dog" "is" "round" "+")
((triple1) -> (rule3 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
((triple16) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
((triple11) -> (rule3 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
((triple14) -> (rule3 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
((((triple16) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
((((triple11) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
((((triple14) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
((((((triple16) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3