The dog needs the mouse. The dog needs the rabbit. The mouse chases the rabbit. The mouse sees the dog. The rabbit chases the squirrel. The rabbit is young. The rabbit needs the mouse. The rabbit sees the mouse. The squirrel is red. The squirrel sees the mouse. If someone is young then they chase the dog. If someone needs the rabbit and they need the dog then the dog is red. If someone sees the mouse and the mouse sees the rabbit then the mouse chases the dog. If the rabbit sees the dog then the dog needs the squirrel. If someone is kind then they need the dog. If someone is red then they see the mouse. If someone chases the dog then the dog is kind. If the dog sees the rabbit and the dog is nice then the rabbit chases the mouse.
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
If someone is young then they chase the dog.
((("someone" "is" "young" "+")) -> ("someone" "chases" "dog" "+"))
If someone needs the rabbit and they need the dog then the dog is red.
((("someone" "needs" "rabbit" "+") ("someone" "needs" "dog" "+")) -> ("dog" "is" "red" "+"))
If someone sees the mouse and the mouse sees the rabbit then the mouse chases the dog.
((("someone" "sees" "mouse" "+") ("mouse" "sees" "rabbit" "+")) -> ("mouse" "chases" "dog" "+"))
If the rabbit sees the dog then the dog needs the squirrel.
((("rabbit" "sees" "dog" "+")) -> ("dog" "needs" "squirrel" "+"))
If someone is kind then they need the dog.
((("someone" "is" "kind" "+")) -> ("someone" "needs" "dog" "+"))
If someone is red then they see the mouse.
((("someone" "is" "red" "+")) -> ("someone" "sees" "mouse" "+"))
If someone chases the dog then the dog is kind.
((("someone" "chases" "dog" "+")) -> ("dog" "is" "kind" "+"))
If the dog sees the rabbit and the dog is nice then the rabbit chases the mouse.
((("dog" "sees" "rabbit" "+") ("dog" "is" "nice" "+")) -> ("rabbit" "chases" "mouse" "+"))
The squirrel is red.
True
1
proof
[(triple9)]
("squirrel" "is" "red" "+")
triple9
The rabbit does not chase the squirrel.
False
1
inv-proof
[(triple5)]
("rabbit" "chases" "squirrel" "-")
triple5
The rabbit chases the dog.
True
2
proof
[(((triple6) -> rule1))]
("rabbit" "chases" "dog" "+")
((triple6) -> (rule1 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The rabbit does not chase the dog.
False
2
inv-proof
[(((triple6) -> rule1))]
("rabbit" "chases" "dog" "-")
((triple6) -> (rule1 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The dog is kind.
True
3
proof
[(((((triple6) -> rule1)) -> rule7))]
("dog" "is" "kind" "+")
((((triple6) -> (rule1 % int2))) -> (rule7 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The dog is not kind.
False
3
inv-proof
[(((((triple6) -> rule1)) -> rule7))]
("dog" "is" "kind" "-")
((((triple6) -> (rule1 % int2))) -> (rule7 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The dog needs the dog.
True
4
proof
[(((((((triple6) -> rule1)) -> rule7)) -> rule5))]
("dog" "needs" "dog" "+")
((((((triple6) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int3
The dog does not need the dog.
False
4
inv-proof
[(((((((triple6) -> rule1)) -> rule7)) -> rule5))]
("dog" "needs" "dog" "-")
((((((triple6) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int3
The dog is red.
True
6
proof
[(((triple2 ((((((triple6) -> rule1)) -> rule7)) -> rule5)) -> rule2))]
("dog" "is" "red" "+")
((triple2 ((((((triple6) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
int3
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int4
The dog is not red.
False
6
inv-proof
[(((triple2 ((((((triple6) -> rule1)) -> rule7)) -> rule5)) -> rule2))]
("dog" "is" "red" "-")
((triple2 ((((((triple6) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
int3
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int4
The dog sees the mouse.
True
7
proof
[(((((triple2 ((((((triple6) -> rule1)) -> rule7)) -> rule5)) -> rule2)) -> rule6))]
("dog" "sees" "mouse" "+")
((((triple2 ((((((triple6) -> (rule1 % int5))) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
int3
The dog is kind.
("dog" "is" "kind" "+")
int4
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int5
The dog does not see the mouse.
False
7
inv-proof
[(((((triple2 ((((((triple6) -> rule1)) -> rule7)) -> rule5)) -> rule2)) -> rule6))]
("dog" "sees" "mouse" "-")
((((triple2 ((((((triple6) -> (rule1 % int5))) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
int3
The dog is kind.
("dog" "is" "kind" "+")
int4
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int5
The dog does not need the squirrel.
Unknown
inv-rconc
[@1: The dog needs the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "needs" "squirrel" "-")
The dog chases the dog.
Unknown
rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "chases" "dog" "+")
The rabbit does not need the dog.
Unknown
inv-rconc
[@1: The rabbit needs the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "needs" "dog" "-")
The mouse needs the dog.
Unknown
rconc
[@1: The mouse needs the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "needs" "dog" "+")
The mouse does not chase the dog.
Unknown
inv-rconc
[@1: The mouse chases the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "chases" "dog" "-")
The squirrel needs the dog.
Unknown
rconc
[@1: The squirrel needs the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "needs" "dog" "+")
The dog does not chase the squirrel.
Unknown
inv-random
[@0: The dog chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "squirrel" "-")
The rabbit is nice.
Unknown
random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "+")
The squirrel is not young.
Unknown
inv-random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
The rabbit does not see the squirrel.
Unknown
inv-random
[@0: The rabbit sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "squirrel" "-")
The squirrel chases the mouse.
Unknown
random
[@0: The squirrel chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "mouse" "+")
@0: The dog needs the mouse.[(triple1)] The dog needs the rabbit.[(triple2)] The mouse chases the rabbit.[(triple3)] The mouse sees the dog.[(triple4)] The rabbit chases the squirrel.[(triple5)] The rabbit is young.[(triple6)] The rabbit needs the mouse.[(triple7)] The rabbit sees the mouse.[(triple8)] The squirrel is red.[(triple9)] The squirrel sees the mouse.[(triple10 OR ((triple9) -> rule6))] @1: The rabbit chases the dog.[(((triple6) -> rule1))] @2: The dog is kind.[(((((triple6) -> rule1)) -> rule7))] @3: The dog needs the dog.[(((((((triple6) -> rule1)) -> rule7)) -> rule5))] @4: The dog is red.[(((triple2 ((((((triple6) -> rule1)) -> rule7)) -> rule5)) -> rule2))] @5: The dog sees the mouse.[(((((triple2 ((((((triple6) -> rule1)) -> rule7)) -> rule5)) -> rule2)) -> rule6))]
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple2
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple3
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple4
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
triple5
The rabbit is young.
("rabbit" "is" "young" "+")
triple6
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple7
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple8
The squirrel is red.
("squirrel" "is" "red" "+")
triple9
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple10
((triple9) -> (rule6 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
((triple6) -> (rule1 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
((((triple6) -> (rule1 % int2))) -> (rule7 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
((((((triple6) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int3
The dog is red.
("dog" "is" "red" "+")
((triple2 ((((((triple6) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
int3
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int4
The dog sees the mouse.
("dog" "sees" "mouse" "+")
((((triple2 ((((((triple6) -> (rule1 % int5))) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
int3
The dog is kind.
("dog" "is" "kind" "+")
int4
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int5