The cat chases the cow. The cat is rough. The cat needs the rabbit. The cow does not chase the cat. The cow chases the rabbit. The cow eats the cat. The cow eats the mouse. The mouse chases the cow. The mouse is red. The mouse needs the cow. The rabbit is big. The rabbit needs the cow. If someone needs the rabbit then they chase the mouse. If the cow needs the rabbit and the rabbit eats the cow then the cow is young. Red people are young. If someone is young and they chase the rabbit then they eat the cat. All red people are big. If someone chases the mouse then the mouse is rough. If someone eats the cat and they chase the cow then the cat is kind. If someone chases the mouse and they do not chase the cow then the cow is big. If someone is rough then they chase the rabbit.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The cow does not chase the cat.
("cow" "chases" "cat" "-")
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
If someone needs the rabbit then they chase the mouse.
((("someone" "needs" "rabbit" "+")) -> ("someone" "chases" "mouse" "+"))
If the cow needs the rabbit and the rabbit eats the cow then the cow is young.
((("cow" "needs" "rabbit" "+") ("rabbit" "eats" "cow" "+")) -> ("cow" "is" "young" "+"))
Red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone is young and they chase the rabbit then they eat the cat.
((("someone" "is" "young" "+") ("someone" "chases" "rabbit" "+")) -> ("someone" "eats" "cat" "+"))
All red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone chases the mouse then the mouse is rough.
((("someone" "chases" "mouse" "+")) -> ("mouse" "is" "rough" "+"))
If someone eats the cat and they chase the cow then the cat is kind.
((("someone" "eats" "cat" "+") ("someone" "chases" "cow" "+")) -> ("cat" "is" "kind" "+"))
If someone chases the mouse and they do not chase the cow then the cow is big.
((("someone" "chases" "mouse" "+") ("someone" "chases" "cow" "~")) -> ("cow" "is" "big" "+"))
If someone is rough then they chase the rabbit.
((("someone" "is" "rough" "+")) -> ("someone" "chases" "rabbit" "+"))
The cat needs the rabbit.
True
1
proof
[(triple3)]
("cat" "needs" "rabbit" "+")
triple3
The cow does not eat the cat.
False
1
inv-proof
[(triple6)]
("cow" "eats" "cat" "-")
triple6
The mouse is young.
True
2
proof
[(((triple9) -> rule3))]
("mouse" "is" "young" "+")
((triple9) -> (rule3 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The cat does not chase the mouse.
False
2
inv-proof
[(((triple3) -> rule1))]
("cat" "chases" "mouse" "-")
((triple3) -> (rule1 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The mouse is rough.
True
3
proof
[(((((triple3) -> rule1)) -> rule6))]
("mouse" "is" "rough" "+")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The mouse is not rough.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule6))]
("mouse" "is" "rough" "-")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The mouse chases the rabbit.
True
4
proof
[(((((((triple3) -> rule1)) -> rule6)) -> rule9))]
("mouse" "chases" "rabbit" "+")
((((((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int3
The mouse does not chase the rabbit.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule6)) -> rule9))]
("mouse" "chases" "rabbit" "-")
((((((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int3
The mouse eats the cat.
True
7
proof
[(((((triple9) -> rule3) ((((((triple3) -> rule1)) -> rule6)) -> rule9)) -> rule4))]
("mouse" "eats" "cat" "+")
((((triple9) -> (rule3 % int5)) ((((((triple3) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int4
The mouse is young.
("mouse" "is" "young" "+")
int5
The mouse does not eat the cat.
False
7
inv-proof
[(((((triple9) -> rule3) ((((((triple3) -> rule1)) -> rule6)) -> rule9)) -> rule4))]
("mouse" "eats" "cat" "-")
((((triple9) -> (rule3 % int5)) ((((((triple3) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int4
The mouse is young.
("mouse" "is" "young" "+")
int5
The cat is kind.
True
9
proof
[(((((((triple9) -> rule3) ((((((triple3) -> rule1)) -> rule6)) -> rule9)) -> rule4) triple8) -> rule7))]
("cat" "is" "kind" "+")
((((((triple9) -> (rule3 % int6)) ((((((triple3) -> (rule1 % int5))) -> (rule6 % int4))) -> (rule9 % int3))) -> (rule4 % int2)) triple8) -> (rule7 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int2
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
int4
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int5
The mouse is young.
("mouse" "is" "young" "+")
int6
The cat is not kind.
False
9
inv-proof
[(((((((triple9) -> rule3) ((((((triple3) -> rule1)) -> rule6)) -> rule9)) -> rule4) triple8) -> rule7))]
("cat" "is" "kind" "-")
((((((triple9) -> (rule3 % int6)) ((((((triple3) -> (rule1 % int5))) -> (rule6 % int4))) -> (rule9 % int3))) -> (rule4 % int2)) triple8) -> (rule7 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int2
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
int4
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int5
The mouse is young.
("mouse" "is" "young" "+")
int6
The rabbit does not chase the rabbit.
Unknown
inv-rconc
[@1: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("rabbit" "chases" "rabbit" "-")
The cat eats the cat.
Unknown
rconc
[@2: The cat eats the cat.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("cat" "eats" "cat" "+")
The cow does not chase the mouse.
Unknown
inv-rconc
[@1: The cow chases the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "chases" "mouse" "-")
The mouse chases the mouse.
Unknown
rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "chases" "mouse" "+")
The cow is not young.
Unknown
inv-rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "young" "-")
The cat is young.
Unknown
rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "young" "+")
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The mouse needs the rabbit.
Unknown
random
[@0: The mouse needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "rabbit" "+")
@0: The cat chases the cow.[(triple1)] The cat is rough.[(triple2)] The cat needs the rabbit.[(triple3)] The cow chases the rabbit.[(triple5)] The cow does not chase the cat.[(triple4)] The cow eats the cat.[(triple6)] The cow eats the mouse.[(triple7)] The mouse chases the cow.[(triple8)] The mouse is red.[(triple9)] The mouse needs the cow.[(triple10)] The rabbit is big.[(triple11)] The rabbit needs the cow.[(triple12)] @1: The cat chases the mouse.[(((triple3) -> rule1))] The cat chases the rabbit.[(((triple2) -> rule9))] The mouse is big.[(((triple9) -> rule5))] The mouse is young.[(((triple9) -> rule3))] @2: The mouse is rough.[(((((triple3) -> rule1)) -> rule6))] @3: The mouse chases the rabbit.[(((((((triple3) -> rule1)) -> rule6)) -> rule9))] @4: The mouse eats the cat.[(((((triple9) -> rule3) ((((((triple3) -> rule1)) -> rule6)) -> rule9)) -> rule4))] @5: The cat is kind.[(((((((triple9) -> rule3) ((((((triple3) -> rule1)) -> rule6)) -> rule9)) -> rule4) triple8) -> rule7))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple3
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple5
The cow does not chase the cat.
("cow" "chases" "cat" "-")
triple4
The cow eats the cat.
("cow" "eats" "cat" "+")
triple6
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple7
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple8
The mouse is red.
("mouse" "is" "red" "+")
triple9
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple10
The rabbit is big.
("rabbit" "is" "big" "+")
triple11
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple12
The cat chases the mouse.
("cat" "chases" "mouse" "+")
((triple3) -> (rule1 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
((triple2) -> (rule9 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
((triple9) -> (rule5 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
((triple9) -> (rule3 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
((((((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int3
The mouse eats the cat.
("mouse" "eats" "cat" "+")
((((triple9) -> (rule3 % int5)) ((((((triple3) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int4
The mouse is young.
("mouse" "is" "young" "+")
int5
The cat is kind.
("cat" "is" "kind" "+")
((((((triple9) -> (rule3 % int6)) ((((((triple3) -> (rule1 % int5))) -> (rule6 % int4))) -> (rule9 % int3))) -> (rule4 % int2)) triple8) -> (rule7 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int2
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
int4
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int5
The mouse is young.
("mouse" "is" "young" "+")
int6