The bear chases the squirrel. The bear is not big. The bear is blue. The bear is not round. The bear sees the dog. The dog chases the bear. The dog sees the squirrel. The mouse chases the bear. The squirrel chases the dog. The squirrel likes the dog. If something chases the squirrel then it sees the mouse. If something likes the squirrel then the squirrel likes the mouse. If the dog sees the bear and the dog is not blue then the bear does not see the mouse. If something sees the bear and it does not chase the squirrel then it sees the squirrel. If something is big then it sees the squirrel. If something sees the squirrel and the squirrel is round then it chases the dog. If something sees the mouse then it likes the mouse. If the dog chases the bear then the bear sees the squirrel. If something likes the mouse then it likes the squirrel.
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The bear is not big.
("bear" "is" "big" "-")
The bear is blue.
("bear" "is" "blue" "+")
The bear is not round.
("bear" "is" "round" "-")
The bear sees the dog.
("bear" "sees" "dog" "+")
The dog chases the bear.
("dog" "chases" "bear" "+")
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
If something chases the squirrel then it sees the mouse.
((("something" "chases" "squirrel" "+")) -> ("something" "sees" "mouse" "+"))
If something likes the squirrel then the squirrel likes the mouse.
((("something" "likes" "squirrel" "+")) -> ("squirrel" "likes" "mouse" "+"))
If the dog sees the bear and the dog is not blue then the bear does not see the mouse.
((("dog" "sees" "bear" "+") ("dog" "is" "blue" "~")) -> ("bear" "sees" "mouse" "-"))
If something sees the bear and it does not chase the squirrel then it sees the squirrel.
((("something" "sees" "bear" "+") ("something" "chases" "squirrel" "~")) -> ("something" "sees" "squirrel" "+"))
If something is big then it sees the squirrel.
((("something" "is" "big" "+")) -> ("something" "sees" "squirrel" "+"))
If something sees the squirrel and the squirrel is round then it chases the dog.
((("something" "sees" "squirrel" "+") ("squirrel" "is" "round" "+")) -> ("something" "chases" "dog" "+"))
If something sees the mouse then it likes the mouse.
((("something" "sees" "mouse" "+")) -> ("something" "likes" "mouse" "+"))
If the dog chases the bear then the bear sees the squirrel.
((("dog" "chases" "bear" "+")) -> ("bear" "sees" "squirrel" "+"))
If something likes the mouse then it likes the squirrel.
((("something" "likes" "mouse" "+")) -> ("something" "likes" "squirrel" "+"))
The bear is not round.
True
1
proof
[(triple4)]
("bear" "is" "round" "-")
triple4
The bear is not blue.
False
1
inv-proof
[(triple3)]
("bear" "is" "blue" "-")
triple3
The bear sees the squirrel.
True
2
proof
[(((triple6) -> rule8))]
("bear" "sees" "squirrel" "+")
((triple6) -> (rule8 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear does not see the squirrel.
False
2
inv-proof
[(((triple6) -> rule8))]
("bear" "sees" "squirrel" "-")
((triple6) -> (rule8 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear likes the mouse.
True
3
proof
[(((((triple1) -> rule1)) -> rule7))]
("bear" "likes" "mouse" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int2
The bear does not like the mouse.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule7))]
("bear" "likes" "mouse" "-")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int2
The bear likes the squirrel.
True
4
proof
[(((((((triple1) -> rule1)) -> rule7)) -> rule9))]
("bear" "likes" "squirrel" "+")
((((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int3
The bear does not like the squirrel.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule7)) -> rule9))]
("bear" "likes" "squirrel" "-")
((((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int3
The squirrel likes the mouse.
True
5
proof
[(((((((((triple1) -> rule1)) -> rule7)) -> rule9)) -> rule2))]
("squirrel" "likes" "mouse" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int3
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int4
The squirrel does not like the mouse.
False
5
inv-proof
[(((((((((triple1) -> rule1)) -> rule7)) -> rule9)) -> rule2))]
("squirrel" "likes" "mouse" "-")
((((((((triple1) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int3
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int4
The squirrel likes the squirrel.
True
6
proof
[(((((((((((triple1) -> rule1)) -> rule7)) -> rule9)) -> rule2)) -> rule9))]
("squirrel" "likes" "squirrel" "+")
((((((((((triple1) -> (rule1 % int5))) -> (rule7 % int4))) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int2
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int3
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int4
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int5
The squirrel does not like the squirrel.
False
6
inv-proof
[(((((((((((triple1) -> rule1)) -> rule7)) -> rule9)) -> rule2)) -> rule9))]
("squirrel" "likes" "squirrel" "-")
((((((((((triple1) -> (rule1 % int5))) -> (rule7 % int4))) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int2
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int3
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int4
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int5
The mouse does not like the mouse.
Unknown
inv-rconc
[@2: The mouse likes the mouse.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("mouse" "likes" "mouse" "-")
The mouse sees the squirrel.
Unknown
rconc
[@1: The mouse sees the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "sees" "squirrel" "+")
The dog does not like the squirrel.
Unknown
inv-rconc
[@3: The dog likes the squirrel.[CWA. Example of deepest failure = (rule9 <- rule7 <- rule1 <- FAIL)]]
("dog" "likes" "squirrel" "-")
The squirrel sees the squirrel.
Unknown
rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "sees" "squirrel" "+")
The dog does not chase the dog.
Unknown
inv-rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "chases" "dog" "-")
The bear chases the dog.
Unknown
rconc
[@1: The bear chases the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "chases" "dog" "+")
The squirrel does not see the dog.
Unknown
inv-random
[@0: The squirrel sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "dog" "-")
The mouse sees the bear.
Unknown
random
[@0: The mouse sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "bear" "+")
The squirrel is not big.
Unknown
inv-random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "-")
The dog is round.
Unknown
random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "+")
The dog is not red.
Unknown
inv-random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "-")
The dog sees the bear.
Unknown
random
[@0: The dog sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "bear" "+")
@0: The bear chases the squirrel.[(triple1)] The bear is blue.[(triple3)] The bear is not big.[(triple2)] The bear is not round.[(triple4)] The bear sees the dog.[(triple5)] The dog chases the bear.[(triple6)] The dog sees the squirrel.[(triple7)] The mouse chases the bear.[(triple8)] The squirrel chases the dog.[(triple9)] The squirrel likes the dog.[(triple10)] @1: The bear sees the mouse.[(((triple1) -> rule1))] The bear sees the squirrel.[(((triple6) -> rule8))] @2: The bear likes the mouse.[(((((triple1) -> rule1)) -> rule7))] @3: The bear likes the squirrel.[(((((((triple1) -> rule1)) -> rule7)) -> rule9))] @4: The squirrel likes the mouse.[(((((((((triple1) -> rule1)) -> rule7)) -> rule9)) -> rule2))] @5: The squirrel likes the squirrel.[(((((((((((triple1) -> rule1)) -> rule7)) -> rule9)) -> rule2)) -> rule9))]
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple1
The bear is blue.
("bear" "is" "blue" "+")
triple3
The bear is not big.
("bear" "is" "big" "-")
triple2
The bear is not round.
("bear" "is" "round" "-")
triple4
The bear sees the dog.
("bear" "sees" "dog" "+")
triple5
The dog chases the bear.
("dog" "chases" "bear" "+")
triple6
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple7
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple8
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
triple9
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
triple10
The bear sees the mouse.
("bear" "sees" "mouse" "+")
((triple1) -> (rule1 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
((triple6) -> (rule8 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int2
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
((((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int3
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int3
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int4
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((((((((((triple1) -> (rule1 % int5))) -> (rule7 % int4))) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int2
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int3
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int4
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int5