The dog chases the squirrel. The dog is rough. The dog does not like the rabbit. The mouse is nice. The mouse does not need the squirrel. The rabbit does not chase the mouse. The rabbit is not rough. The rabbit needs the mouse. The rabbit needs the squirrel. The squirrel does not chase the rabbit. The squirrel is blue. The squirrel is rough. The squirrel likes the dog. The squirrel needs the mouse. If something chases the dog and it needs the mouse then the dog is blue. All blue things are round. If something is round then it chases the dog. If the squirrel needs the dog then the dog does not chase the mouse. If something is blue then it chases the squirrel. If something chases the rabbit and it chases the mouse then the rabbit is round. If the squirrel is round and the squirrel needs the rabbit then the squirrel is nice. If the squirrel needs the dog then the dog is nice. If something likes the rabbit and it is not nice then the rabbit needs the dog.
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog does not like the rabbit.
("dog" "likes" "rabbit" "-")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse does not need the squirrel.
("mouse" "needs" "squirrel" "-")
The rabbit does not chase the mouse.
("rabbit" "chases" "mouse" "-")
The rabbit is not rough.
("rabbit" "is" "rough" "-")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
The squirrel does not chase the rabbit.
("squirrel" "chases" "rabbit" "-")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
If something chases the dog and it needs the mouse then the dog is blue.
((("something" "chases" "dog" "+") ("something" "needs" "mouse" "+")) -> ("dog" "is" "blue" "+"))
All blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If something is round then it chases the dog.
((("something" "is" "round" "+")) -> ("something" "chases" "dog" "+"))
If the squirrel needs the dog then the dog does not chase the mouse.
((("squirrel" "needs" "dog" "+")) -> ("dog" "chases" "mouse" "-"))
If something is blue then it chases the squirrel.
((("something" "is" "blue" "+")) -> ("something" "chases" "squirrel" "+"))
If something chases the rabbit and it chases the mouse then the rabbit is round.
((("something" "chases" "rabbit" "+") ("something" "chases" "mouse" "+")) -> ("rabbit" "is" "round" "+"))
If the squirrel is round and the squirrel needs the rabbit then the squirrel is nice.
((("squirrel" "is" "round" "+") ("squirrel" "needs" "rabbit" "+")) -> ("squirrel" "is" "nice" "+"))
If the squirrel needs the dog then the dog is nice.
((("squirrel" "needs" "dog" "+")) -> ("dog" "is" "nice" "+"))
If something likes the rabbit and it is not nice then the rabbit needs the dog.
((("something" "likes" "rabbit" "+") ("something" "is" "nice" "~")) -> ("rabbit" "needs" "dog" "+"))
The squirrel does not chase the rabbit.
True
1
proof
[(triple10)]
("squirrel" "chases" "rabbit" "-")
triple10
The rabbit is rough.
False
1
inv-proof
[(triple7)]
("rabbit" "is" "rough" "+")
triple7
The squirrel chases the squirrel.
True
2
proof
[(((triple11) -> rule5))]
("squirrel" "chases" "squirrel" "+")
((triple11) -> (rule5 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel does not chase the squirrel.
False
2
inv-proof
[(((triple11) -> rule5))]
("squirrel" "chases" "squirrel" "-")
((triple11) -> (rule5 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel chases the dog.
True
3
proof
[(((((triple11) -> rule2)) -> rule3))]
("squirrel" "chases" "dog" "+")
((((triple11) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The squirrel does not chase the dog.
False
3
inv-proof
[(((((triple11) -> rule2)) -> rule3))]
("squirrel" "chases" "dog" "-")
((((triple11) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The dog is blue.
True
5
proof
[(((((((triple11) -> rule2)) -> rule3) triple14) -> rule1))]
("dog" "is" "blue" "+")
((((((triple11) -> (rule2 % int3))) -> (rule3 % int2)) triple14) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The dog is not blue.
False
5
inv-proof
[(((((((triple11) -> rule2)) -> rule3) triple14) -> rule1))]
("dog" "is" "blue" "-")
((((((triple11) -> (rule2 % int3))) -> (rule3 % int2)) triple14) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The dog is round.
True
6
proof
[(((((((((triple11) -> rule2)) -> rule3) triple14) -> rule1)) -> rule2))]
("dog" "is" "round" "+")
((((((((triple11) -> (rule2 % int4))) -> (rule3 % int3)) triple14) -> (rule1 % int2))) -> (rule2 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int3
The squirrel is round.
("squirrel" "is" "round" "+")
int4
The dog is not round.
False
6
inv-proof
[(((((((((triple11) -> rule2)) -> rule3) triple14) -> rule1)) -> rule2))]
("dog" "is" "round" "-")
((((((((triple11) -> (rule2 % int4))) -> (rule3 % int3)) triple14) -> (rule1 % int2))) -> (rule2 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int3
The squirrel is round.
("squirrel" "is" "round" "+")
int4
The dog chases the dog.
True
7
proof
[(((((((((((triple11) -> rule2)) -> rule3) triple14) -> rule1)) -> rule2)) -> rule3))]
("dog" "chases" "dog" "+")
((((((((((triple11) -> (rule2 % int5))) -> (rule3 % int4)) triple14) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int4
The squirrel is round.
("squirrel" "is" "round" "+")
int5
The dog does not chase the dog.
False
7
inv-proof
[(((((((((((triple11) -> rule2)) -> rule3) triple14) -> rule1)) -> rule2)) -> rule3))]
("dog" "chases" "dog" "-")
((((((((((triple11) -> (rule2 % int5))) -> (rule3 % int4)) triple14) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int4
The squirrel is round.
("squirrel" "is" "round" "+")
int5
The rabbit does not chase the dog.
Unknown
inv-rconc
[@2: The rabbit chases the dog.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("rabbit" "chases" "dog" "-")
The rabbit needs the dog.
Unknown
rconc
[@1: The rabbit needs the dog.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("rabbit" "needs" "dog" "+")
The mouse is not round.
Unknown
inv-rconc
[@1: The mouse is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "round" "-")
The dog is nice.
Unknown
rconc
[@1: The dog is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "is" "nice" "+")
The mouse does not chase the dog.
Unknown
inv-rconc
[@2: The mouse chases the dog.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("mouse" "chases" "dog" "-")
The rabbit chases the squirrel.
Unknown
rconc
[@1: The rabbit chases the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "chases" "squirrel" "+")
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The squirrel likes the rabbit.
Unknown
random
[@0: The squirrel likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "rabbit" "+")
The rabbit does not like the dog.
Unknown
inv-random
[@0: The rabbit likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "dog" "-")
The mouse chases the rabbit.
Unknown
random
[@0: The mouse chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "rabbit" "+")
The dog does not need the squirrel.
Unknown
inv-random
[@0: The dog needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "squirrel" "-")
The rabbit is nice.
Unknown
random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "+")
@0: The dog chases the squirrel.[(triple1 OR ((((((((triple11) -> rule2)) -> rule3) triple14) -> rule1)) -> rule5))] The dog does not like the rabbit.[(triple3)] The dog is rough.[(triple2)] The mouse does not need the squirrel.[(triple5)] The mouse is nice.[(triple4)] The rabbit does not chase the mouse.[(triple6)] The rabbit is not rough.[(triple7)] The rabbit needs the mouse.[(triple8)] The rabbit needs the squirrel.[(triple9)] The squirrel does not chase the rabbit.[(triple10)] The squirrel is blue.[(triple11)] The squirrel is rough.[(triple12)] The squirrel likes the dog.[(triple13)] The squirrel needs the mouse.[(triple14)] @1: The squirrel chases the squirrel.[(((triple11) -> rule5))] The squirrel is round.[(((triple11) -> rule2))] @2: The squirrel chases the dog.[(((((triple11) -> rule2)) -> rule3))] @3: The dog is blue.[(((((((triple11) -> rule2)) -> rule3) triple14) -> rule1))] @4: The dog is round.[(((((((((triple11) -> rule2)) -> rule3) triple14) -> rule1)) -> rule2))] @5: The dog chases the dog.[(((((((((((triple11) -> rule2)) -> rule3) triple14) -> rule1)) -> rule2)) -> rule3))]
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
triple1
((((((((triple11) -> (rule2 % int4))) -> (rule3 % int3)) triple14) -> (rule1 % int2))) -> (rule5 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int3
The squirrel is round.
("squirrel" "is" "round" "+")
int4
The dog does not like the rabbit.
("dog" "likes" "rabbit" "-")
triple3
The dog is rough.
("dog" "is" "rough" "+")
triple2
The mouse does not need the squirrel.
("mouse" "needs" "squirrel" "-")
triple5
The mouse is nice.
("mouse" "is" "nice" "+")
triple4
The rabbit does not chase the mouse.
("rabbit" "chases" "mouse" "-")
triple6
The rabbit is not rough.
("rabbit" "is" "rough" "-")
triple7
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple8
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
triple9
The squirrel does not chase the rabbit.
("squirrel" "chases" "rabbit" "-")
triple10
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple11
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple12
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
triple13
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple14
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((triple11) -> (rule5 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
((triple11) -> (rule2 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
((((triple11) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
((((((triple11) -> (rule2 % int3))) -> (rule3 % int2)) triple14) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The dog is round.
("dog" "is" "round" "+")
((((((((triple11) -> (rule2 % int4))) -> (rule3 % int3)) triple14) -> (rule1 % int2))) -> (rule2 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int3
The squirrel is round.
("squirrel" "is" "round" "+")
int4
The dog chases the dog.
("dog" "chases" "dog" "+")
((((((((((triple11) -> (rule2 % int5))) -> (rule3 % int4)) triple14) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int4
The squirrel is round.
("squirrel" "is" "round" "+")
int5