The cat eats the mouse. The cat is red. The dog chases the cat. The dog chases the mouse. The mouse chases the rabbit. The mouse is red. The mouse sees the cat. The rabbit eats the cat. The rabbit eats the dog. The rabbit eats the mouse. The rabbit sees the dog. The rabbit sees the mouse. If something sees the rabbit then the rabbit sees the mouse. If something chases the rabbit then it chases the dog. If the rabbit eats the mouse then the rabbit is rough. If something eats the dog then it eats the rabbit. If the dog chases the cat then the dog is cold. If something eats the mouse and the mouse chases the cat then it chases the rabbit. If something sees the cat then the cat eats the dog. If the mouse sees the rabbit then the mouse eats the dog. If something chases the dog then it chases the cat.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is red.
("cat" "is" "red" "+")
The dog chases the cat.
("dog" "chases" "cat" "+")
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If something sees the rabbit then the rabbit sees the mouse.
((("something" "sees" "rabbit" "+")) -> ("rabbit" "sees" "mouse" "+"))
If something chases the rabbit then it chases the dog.
((("something" "chases" "rabbit" "+")) -> ("something" "chases" "dog" "+"))
If the rabbit eats the mouse then the rabbit is rough.
((("rabbit" "eats" "mouse" "+")) -> ("rabbit" "is" "rough" "+"))
If something eats the dog then it eats the rabbit.
((("something" "eats" "dog" "+")) -> ("something" "eats" "rabbit" "+"))
If the dog chases the cat then the dog is cold.
((("dog" "chases" "cat" "+")) -> ("dog" "is" "cold" "+"))
If something eats the mouse and the mouse chases the cat then it chases the rabbit.
((("something" "eats" "mouse" "+") ("mouse" "chases" "cat" "+")) -> ("something" "chases" "rabbit" "+"))
If something sees the cat then the cat eats the dog.
((("something" "sees" "cat" "+")) -> ("cat" "eats" "dog" "+"))
If the mouse sees the rabbit then the mouse eats the dog.
((("mouse" "sees" "rabbit" "+")) -> ("mouse" "eats" "dog" "+"))
If something chases the dog then it chases the cat.
((("something" "chases" "dog" "+")) -> ("something" "chases" "cat" "+"))
The rabbit eats the cat.
True
1
proof
[(triple8)]
("rabbit" "eats" "cat" "+")
triple8
The mouse does not see the cat.
False
1
inv-proof
[(triple7)]
("mouse" "sees" "cat" "-")
triple7
The cat eats the dog.
True
2
proof
[(((triple7) -> rule7))]
("cat" "eats" "dog" "+")
((triple7) -> (rule7 % int1))
The cat eats the dog.
("cat" "eats" "dog" "+")
int1
The rabbit is not rough.
False
2
inv-proof
[(((triple10) -> rule3))]
("rabbit" "is" "rough" "-")
((triple10) -> (rule3 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The cat eats the rabbit.
True
3
proof
[(((((triple7) -> rule7)) -> rule4))]
("cat" "eats" "rabbit" "+")
((((triple7) -> (rule7 % int2))) -> (rule4 % int1))
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int1
The cat eats the dog.
("cat" "eats" "dog" "+")
int2
The cat does not eat the rabbit.
False
3
inv-proof
[(((((triple7) -> rule7)) -> rule4))]
("cat" "eats" "rabbit" "-")
((((triple7) -> (rule7 % int2))) -> (rule4 % int1))
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int1
The cat eats the dog.
("cat" "eats" "dog" "+")
int2
The rabbit chases the rabbit.
True
5
proof
[(((triple10 ((((triple5) -> rule2)) -> rule9)) -> rule6))]
("rabbit" "chases" "rabbit" "+")
((triple10 ((((triple5) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int2
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int3
The cat does not chase the rabbit.
False
5
inv-proof
[(((triple1 ((((triple5) -> rule2)) -> rule9)) -> rule6))]
("cat" "chases" "rabbit" "-")
((triple1 ((((triple5) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int2
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int3
The cat chases the dog.
True
6
proof
[(((((triple1 ((((triple5) -> rule2)) -> rule9)) -> rule6)) -> rule2))]
("cat" "chases" "dog" "+")
((((triple1 ((((triple5) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cat chases the dog.
("cat" "chases" "dog" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int3
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int4
The rabbit does not chase the dog.
False
6
inv-proof
[(((((triple10 ((((triple5) -> rule2)) -> rule9)) -> rule6)) -> rule2))]
("rabbit" "chases" "dog" "-")
((((triple10 ((((triple5) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int3
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int4
The cat chases the cat.
True
7
proof
[(((((((triple1 ((((triple5) -> rule2)) -> rule9)) -> rule6)) -> rule2)) -> rule9))]
("cat" "chases" "cat" "+")
((((((triple1 ((((triple5) -> (rule2 % int5))) -> (rule9 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat chases the dog.
("cat" "chases" "dog" "+")
int2
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int3
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int4
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int5
The cat does not chase the cat.
False
7
inv-proof
[(((((((triple1 ((((triple5) -> rule2)) -> rule9)) -> rule6)) -> rule2)) -> rule9))]
("cat" "chases" "cat" "-")
((((((triple1 ((((triple5) -> (rule2 % int5))) -> (rule9 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat chases the dog.
("cat" "chases" "dog" "+")
int2
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int3
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int4
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int5
The mouse does not eat the dog.
Unknown
inv-rconc
[@1: The mouse eats the dog.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "eats" "dog" "-")
The dog chases the dog.
Unknown
rconc
[@2: The dog chases the dog.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("dog" "chases" "dog" "+")
The mouse does not eat the rabbit.
Unknown
inv-rconc
[@2: The mouse eats the rabbit.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("mouse" "eats" "rabbit" "-")
The dog chases the rabbit.
Unknown
rconc
[@1: The dog chases the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "chases" "rabbit" "+")
The dog does not eat the rabbit.
Unknown
inv-rconc
[@1: The dog eats the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "eats" "rabbit" "-")
The dog is young.
Unknown
random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "+")
The cat is not cold.
Unknown
inv-random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
The dog is not red.
Unknown
inv-random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "-")
The dog eats the cat.
Unknown
random
[@0: The dog eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "cat" "+")
@0: The cat eats the mouse.[(triple1)] The cat is red.[(triple2)] The dog chases the cat.[(triple3)] The dog chases the mouse.[(triple4)] The mouse chases the rabbit.[(triple5)] The mouse is red.[(triple6)] The mouse sees the cat.[(triple7)] The rabbit eats the cat.[(triple8)] The rabbit eats the dog.[(triple9)] The rabbit eats the mouse.[(triple10)] The rabbit sees the dog.[(triple11)] The rabbit sees the mouse.[(triple12)] @1: The cat eats the dog.[(((triple7) -> rule7))] The dog is cold.[(((triple3) -> rule5))] The mouse chases the dog.[(((triple5) -> rule2))] The rabbit eats the rabbit.[(((triple9) -> rule4))] The rabbit is rough.[(((triple10) -> rule3))] @2: The cat eats the rabbit.[(((((triple7) -> rule7)) -> rule4))] The mouse chases the cat.[(((((triple5) -> rule2)) -> rule9))] @3: The cat chases the rabbit.[(((triple1 ((((triple5) -> rule2)) -> rule9)) -> rule6))] The rabbit chases the rabbit.[(((triple10 ((((triple5) -> rule2)) -> rule9)) -> rule6))] @4: The cat chases the dog.[(((((triple1 ((((triple5) -> rule2)) -> rule9)) -> rule6)) -> rule2))] The rabbit chases the dog.[(((((triple10 ((((triple5) -> rule2)) -> rule9)) -> rule6)) -> rule2))] @5: The cat chases the cat.[(((((((triple1 ((((triple5) -> rule2)) -> rule9)) -> rule6)) -> rule2)) -> rule9))] The rabbit chases the cat.[(((((((triple10 ((((triple5) -> rule2)) -> rule9)) -> rule6)) -> rule2)) -> rule9))]
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The cat is red.
("cat" "is" "red" "+")
triple2
The dog chases the cat.
("dog" "chases" "cat" "+")
triple3
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple4
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple5
The mouse is red.
("mouse" "is" "red" "+")
triple6
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple7
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple8
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple9
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple10
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple11
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple12
The cat eats the dog.
("cat" "eats" "dog" "+")
((triple7) -> (rule7 % int1))
The cat eats the dog.
("cat" "eats" "dog" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
((triple3) -> (rule5 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
((triple5) -> (rule2 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((triple9) -> (rule4 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
((triple10) -> (rule3 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
((((triple7) -> (rule7 % int2))) -> (rule4 % int1))
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int1
The cat eats the dog.
("cat" "eats" "dog" "+")
int2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
((((triple5) -> (rule2 % int2))) -> (rule9 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int2
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
((triple1 ((((triple5) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int2
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int3
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple10 ((((triple5) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int2
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int3
The cat chases the dog.
("cat" "chases" "dog" "+")
((((triple1 ((((triple5) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cat chases the dog.
("cat" "chases" "dog" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int3
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int4
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
((((triple10 ((((triple5) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int3
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int4
The cat chases the cat.
("cat" "chases" "cat" "+")
((((((triple1 ((((triple5) -> (rule2 % int5))) -> (rule9 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat chases the dog.
("cat" "chases" "dog" "+")
int2
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int3
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int4
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int5
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
((((((triple10 ((((triple5) -> (rule2 % int5))) -> (rule9 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int3
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int4
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int5