The dog chases the mouse. The dog sees the mouse. The lion is red. The mouse is blue. The mouse is red. The mouse is young. The squirrel eats the lion. If something is red then it sees the dog. If something sees the dog then it eats the squirrel. If something eats the squirrel then the squirrel is blue.
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The lion is red.
("lion" "is" "red" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is young.
("mouse" "is" "young" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
If something is red then it sees the dog.
((("something" "is" "red" "+")) -> ("something" "sees" "dog" "+"))
If something sees the dog then it eats the squirrel.
((("something" "sees" "dog" "+")) -> ("something" "eats" "squirrel" "+"))
If something eats the squirrel then the squirrel is blue.
((("something" "eats" "squirrel" "+")) -> ("squirrel" "is" "blue" "+"))
The mouse is young.
True
1
proof
[(triple6)]
("mouse" "is" "young" "+")
triple6
The mouse is not blue.
False
1
inv-proof
[(triple4)]
("mouse" "is" "blue" "-")
triple4
The mouse sees the dog.
True
2
proof
[(((triple5) -> rule1))]
("mouse" "sees" "dog" "+")
((triple5) -> (rule1 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The lion does not see the dog.
False
2
inv-proof
[(((triple3) -> rule1))]
("lion" "sees" "dog" "-")
((triple3) -> (rule1 % int1))
The lion sees the dog.
("lion" "sees" "dog" "+")
int1
The mouse eats the squirrel.
True
3
proof
[(((((triple5) -> rule1)) -> rule2))]
("mouse" "eats" "squirrel" "+")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
The lion does not eat the squirrel.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("lion" "eats" "squirrel" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int1
The lion sees the dog.
("lion" "sees" "dog" "+")
int2
The squirrel is blue.
True
4
proof
[(((((((triple3) -> rule1)) -> rule2)) -> rule3) OR ((((((triple5) -> rule1)) -> rule2)) -> rule3))]
("squirrel" "is" "blue" "+")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int2
The lion sees the dog.
("lion" "sees" "dog" "+")
int3
((((((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int3
The squirrel is not blue.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule2)) -> rule3) OR ((((((triple5) -> rule1)) -> rule2)) -> rule3))]
("squirrel" "is" "blue" "-")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int2
The lion sees the dog.
("lion" "sees" "dog" "+")
int3
((((((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int3
The squirrel does not eat the squirrel.
Unknown
inv-rconc
[@2: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("squirrel" "eats" "squirrel" "-")
The dog eats the squirrel.
Unknown
rconc
[@2: The dog eats the squirrel.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("dog" "eats" "squirrel" "+")
The dog does not see the dog.
Unknown
inv-rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "sees" "dog" "-")
The squirrel sees the dog.
Unknown
rconc
[@1: The squirrel sees the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "sees" "dog" "+")
The lion does not eat the dog.
Unknown
inv-random
[@0: The lion eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "dog" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
The squirrel is not young.
Unknown
inv-random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
@0: The dog chases the mouse.[(triple1)] The dog sees the mouse.[(triple2)] The lion is red.[(triple3)] The mouse is blue.[(triple4)] The mouse is red.[(triple5)] The mouse is young.[(triple6)] The squirrel eats the lion.[(triple7)] @1: The lion sees the dog.[(((triple3) -> rule1))] The mouse sees the dog.[(((triple5) -> rule1))] @2: The lion eats the squirrel.[(((((triple3) -> rule1)) -> rule2))] The mouse eats the squirrel.[(((((triple5) -> rule1)) -> rule2))] @3: The squirrel is blue.[(((((((triple3) -> rule1)) -> rule2)) -> rule3) OR ((((((triple5) -> rule1)) -> rule2)) -> rule3))]
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple2
The lion is red.
("lion" "is" "red" "+")
triple3
The mouse is blue.
("mouse" "is" "blue" "+")
triple4
The mouse is red.
("mouse" "is" "red" "+")
triple5
The mouse is young.
("mouse" "is" "young" "+")
triple6
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple7
The lion sees the dog.
("lion" "sees" "dog" "+")
((triple3) -> (rule1 % int1))
The lion sees the dog.
("lion" "sees" "dog" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
((triple5) -> (rule1 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int1
The lion sees the dog.
("lion" "sees" "dog" "+")
int2
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int2
The lion sees the dog.
("lion" "sees" "dog" "+")
int3
((((((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int3