The bear is cold. The bear is nice. The dog chases the bear. The dog eats the mouse. The dog is young. The dog needs the bear. The dog needs the mouse. The mouse chases the squirrel. The mouse eats the dog. The mouse eats the squirrel. The mouse is kind. The mouse is young. The squirrel eats the bear. The squirrel eats the dog. Cold things are big. If something chases the mouse then the mouse is cold. If something eats the dog and it chases the dog then the dog eats the mouse. If something is nice then it needs the squirrel. If something is kind then it eats the bear. If something is big then it chases the mouse.
The bear is cold.
("bear" "is" "cold" "+")
The bear is nice.
("bear" "is" "nice" "+")
The dog chases the bear.
("dog" "chases" "bear" "+")
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is young.
("mouse" "is" "young" "+")
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
Cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If something chases the mouse then the mouse is cold.
((("something" "chases" "mouse" "+")) -> ("mouse" "is" "cold" "+"))
If something eats the dog and it chases the dog then the dog eats the mouse.
((("something" "eats" "dog" "+") ("something" "chases" "dog" "+")) -> ("dog" "eats" "mouse" "+"))
If something is nice then it needs the squirrel.
((("something" "is" "nice" "+")) -> ("something" "needs" "squirrel" "+"))
If something is kind then it eats the bear.
((("something" "is" "kind" "+")) -> ("something" "eats" "bear" "+"))
If something is big then it chases the mouse.
((("something" "is" "big" "+")) -> ("something" "chases" "mouse" "+"))
The squirrel eats the bear.
True
1
proof
[(triple13)]
("squirrel" "eats" "bear" "+")
triple13
The squirrel does not eat the dog.
False
1
inv-proof
[(triple14)]
("squirrel" "eats" "dog" "-")
triple14
The bear needs the squirrel.
True
2
proof
[(((triple2) -> rule4))]
("bear" "needs" "squirrel" "+")
((triple2) -> (rule4 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The bear does not need the squirrel.
False
2
inv-proof
[(((triple2) -> rule4))]
("bear" "needs" "squirrel" "-")
((triple2) -> (rule4 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The bear chases the mouse.
True
3
proof
[(((((triple1) -> rule1)) -> rule6))]
("bear" "chases" "mouse" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear does not chase the mouse.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule6))]
("bear" "chases" "mouse" "-")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The mouse is cold.
True
4
proof
[(((((((triple1) -> rule1)) -> rule6)) -> rule2))]
("mouse" "is" "cold" "+")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The bear is big.
("bear" "is" "big" "+")
int3
The mouse is not cold.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule6)) -> rule2))]
("mouse" "is" "cold" "-")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The bear is big.
("bear" "is" "big" "+")
int3
The mouse is big.
True
5
proof
[(((((((((triple1) -> rule1)) -> rule6)) -> rule2)) -> rule1))]
("mouse" "is" "big" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int3
The bear is big.
("bear" "is" "big" "+")
int4
The mouse is not big.
False
5
inv-proof
[(((((((((triple1) -> rule1)) -> rule6)) -> rule2)) -> rule1))]
("mouse" "is" "big" "-")
((((((((triple1) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int3
The bear is big.
("bear" "is" "big" "+")
int4
The mouse chases the mouse.
True
6
proof
[(((((((((((triple1) -> rule1)) -> rule6)) -> rule2)) -> rule1)) -> rule6))]
("mouse" "chases" "mouse" "+")
((((((((((triple1) -> (rule1 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int4
The bear is big.
("bear" "is" "big" "+")
int5
The mouse does not chase the mouse.
False
6
inv-proof
[(((((((((((triple1) -> rule1)) -> rule6)) -> rule2)) -> rule1)) -> rule6))]
("mouse" "chases" "mouse" "-")
((((((((((triple1) -> (rule1 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int4
The bear is big.
("bear" "is" "big" "+")
int5
The dog does not chase the mouse.
Unknown
inv-rconc
[@2: The dog chases the mouse.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("dog" "chases" "mouse" "-")
The squirrel chases the mouse.
Unknown
rconc
[@2: The squirrel chases the mouse.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("squirrel" "chases" "mouse" "+")
The dog is not big.
Unknown
inv-rconc
[@1: The dog is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "big" "-")
The dog eats the bear.
Unknown
rconc
[@1: The dog eats the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "eats" "bear" "+")
The squirrel does not need the squirrel.
Unknown
inv-rconc
[@1: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "needs" "squirrel" "-")
The bear eats the bear.
Unknown
rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "eats" "bear" "+")
The squirrel does not eat the mouse.
Unknown
inv-random
[@0: The squirrel eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "mouse" "-")
The mouse needs the dog.
Unknown
random
[@0: The mouse needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "dog" "+")
The bear does not chase the dog.
Unknown
inv-random
[@0: The bear chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "dog" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "-")
The bear is young.
Unknown
random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "+")
@0: The bear is cold.[(triple1)] The bear is nice.[(triple2)] The dog chases the bear.[(triple3)] The dog eats the mouse.[(triple4)] The dog is young.[(triple5)] The dog needs the bear.[(triple6)] The dog needs the mouse.[(triple7)] The mouse chases the squirrel.[(triple8)] The mouse eats the dog.[(triple9)] The mouse eats the squirrel.[(triple10)] The mouse is kind.[(triple11)] The mouse is young.[(triple12)] The squirrel eats the bear.[(triple13)] The squirrel eats the dog.[(triple14)] @1: The bear is big.[(((triple1) -> rule1))] The bear needs the squirrel.[(((triple2) -> rule4))] The mouse eats the bear.[(((triple11) -> rule5))] @2: The bear chases the mouse.[(((((triple1) -> rule1)) -> rule6))] @3: The mouse is cold.[(((((((triple1) -> rule1)) -> rule6)) -> rule2))] @4: The mouse is big.[(((((((((triple1) -> rule1)) -> rule6)) -> rule2)) -> rule1))] @5: The mouse chases the mouse.[(((((((((((triple1) -> rule1)) -> rule6)) -> rule2)) -> rule1)) -> rule6))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The bear is nice.
("bear" "is" "nice" "+")
triple2
The dog chases the bear.
("dog" "chases" "bear" "+")
triple3
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple4
The dog is young.
("dog" "is" "young" "+")
triple5
The dog needs the bear.
("dog" "needs" "bear" "+")
triple6
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple7
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple8
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple9
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple10
The mouse is kind.
("mouse" "is" "kind" "+")
triple11
The mouse is young.
("mouse" "is" "young" "+")
triple12
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
triple13
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
triple14
The bear is big.
("bear" "is" "big" "+")
((triple1) -> (rule1 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
((triple2) -> (rule4 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The mouse eats the bear.
("mouse" "eats" "bear" "+")
((triple11) -> (rule5 % int1))
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The bear is big.
("bear" "is" "big" "+")
int3
The mouse is big.
("mouse" "is" "big" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int3
The bear is big.
("bear" "is" "big" "+")
int4
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((((((((((triple1) -> (rule1 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int4
The bear is big.
("bear" "is" "big" "+")
int5