The cat is blue. The mouse does not chase the squirrel. The mouse eats the cat. The mouse eats the rabbit. The mouse is big. The mouse sees the rabbit. The mouse sees the squirrel. The rabbit does not chase the cat. The rabbit chases the squirrel. The rabbit is young. The squirrel eats the cat. The squirrel sees the cat. If someone is young and they eat the mouse then the mouse does not chase the rabbit. If someone chases the squirrel then they are young. If someone eats the rabbit then the rabbit sees the squirrel. If someone sees the squirrel then they are green. If someone is green then they chase the mouse. If the rabbit is big and the rabbit does not chase the cat then the rabbit is green. If someone chases the mouse and the mouse eats the cat then they eat the mouse.
The cat is blue.
("cat" "is" "blue" "+")
The mouse does not chase the squirrel.
("mouse" "chases" "squirrel" "-")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
If someone is young and they eat the mouse then the mouse does not chase the rabbit.
((("someone" "is" "young" "+") ("someone" "eats" "mouse" "+")) -> ("mouse" "chases" "rabbit" "-"))
If someone chases the squirrel then they are young.
((("someone" "chases" "squirrel" "+")) -> ("someone" "is" "young" "+"))
If someone eats the rabbit then the rabbit sees the squirrel.
((("someone" "eats" "rabbit" "+")) -> ("rabbit" "sees" "squirrel" "+"))
If someone sees the squirrel then they are green.
((("someone" "sees" "squirrel" "+")) -> ("someone" "is" "green" "+"))
If someone is green then they chase the mouse.
((("someone" "is" "green" "+")) -> ("someone" "chases" "mouse" "+"))
If the rabbit is big and the rabbit does not chase the cat then the rabbit is green.
((("rabbit" "is" "big" "+") ("rabbit" "chases" "cat" "~")) -> ("rabbit" "is" "green" "+"))
If someone chases the mouse and the mouse eats the cat then they eat the mouse.
((("someone" "chases" "mouse" "+") ("mouse" "eats" "cat" "+")) -> ("someone" "eats" "mouse" "+"))
The rabbit chases the squirrel.
True
1
proof
[(triple9)]
("rabbit" "chases" "squirrel" "+")
triple9
The rabbit chases the cat.
False
1
inv-proof
[(triple8)]
("rabbit" "chases" "cat" "+")
triple8
The rabbit sees the squirrel.
True
2
proof
[(((triple4) -> rule3))]
("rabbit" "sees" "squirrel" "+")
((triple4) -> (rule3 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The mouse is not green.
False
2
inv-proof
[(((triple7) -> rule4))]
("mouse" "is" "green" "-")
((triple7) -> (rule4 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse chases the mouse.
True
3
proof
[(((((triple7) -> rule4)) -> rule5))]
("mouse" "chases" "mouse" "+")
((((triple7) -> (rule4 % int2))) -> (rule5 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse does not chase the mouse.
False
3
inv-proof
[(((((triple7) -> rule4)) -> rule5))]
("mouse" "chases" "mouse" "-")
((((triple7) -> (rule4 % int2))) -> (rule5 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The rabbit chases the mouse.
True
4
proof
[(((((((triple4) -> rule3)) -> rule4)) -> rule5))]
("rabbit" "chases" "mouse" "+")
((((((triple4) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int3
The rabbit does not chase the mouse.
False
4
inv-proof
[(((((((triple4) -> rule3)) -> rule4)) -> rule5))]
("rabbit" "chases" "mouse" "-")
((((((triple4) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int3
The rabbit eats the mouse.
True
6
proof
[(((((((((triple4) -> rule3)) -> rule4)) -> rule5) triple3) -> rule7))]
("rabbit" "eats" "mouse" "+")
((((((((triple4) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule5 % int2)) triple3) -> (rule7 % int1))
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int4
The rabbit does not eat the mouse.
False
6
inv-proof
[(((((((((triple4) -> rule3)) -> rule4)) -> rule5) triple3) -> rule7))]
("rabbit" "eats" "mouse" "-")
((((((((triple4) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule5 % int2)) triple3) -> (rule7 % int1))
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int4
The mouse does not chase the rabbit.
True
8
proof
[(((triple10 ((((((((triple4) -> rule3)) -> rule4)) -> rule5) triple3) -> rule7)) -> rule1) OR ((((triple9) -> rule2) ((((((((triple4) -> rule3)) -> rule4)) -> rule5) triple3) -> rule7)) -> rule1))]
("mouse" "chases" "rabbit" "-")
((triple10 ((((((((triple4) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule5 % int3)) triple3) -> (rule7 % int2))) -> (rule1 % int1))
The mouse does not chase the rabbit.
("mouse" "chases" "rabbit" "-")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int3
The rabbit is green.
("rabbit" "is" "green" "+")
int4
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int5
((((triple9) -> (rule2 % int6)) ((((((((triple4) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule5 % int3)) triple3) -> (rule7 % int2))) -> (rule1 % int1))
The mouse does not chase the rabbit.
("mouse" "chases" "rabbit" "-")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int3
The rabbit is green.
("rabbit" "is" "green" "+")
int4
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int5
The rabbit is young.
("rabbit" "is" "young" "+")
int6
The mouse chases the rabbit.
False
8
inv-proof
[(((triple10 ((((((((triple4) -> rule3)) -> rule4)) -> rule5) triple3) -> rule7)) -> rule1) OR ((((triple9) -> rule2) ((((((((triple4) -> rule3)) -> rule4)) -> rule5) triple3) -> rule7)) -> rule1))]
("mouse" "chases" "rabbit" "+")
((triple10 ((((((((triple4) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule5 % int3)) triple3) -> (rule7 % int2))) -> (rule1 % int1))
The mouse does not chase the rabbit.
("mouse" "chases" "rabbit" "-")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int3
The rabbit is green.
("rabbit" "is" "green" "+")
int4
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int5
((((triple9) -> (rule2 % int6)) ((((((((triple4) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule5 % int3)) triple3) -> (rule7 % int2))) -> (rule1 % int1))
The mouse does not chase the rabbit.
("mouse" "chases" "rabbit" "-")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int3
The rabbit is green.
("rabbit" "is" "green" "+")
int4
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int5
The rabbit is young.
("rabbit" "is" "young" "+")
int6
The squirrel does not chase the mouse.
Unknown
inv-rconc
[@2: The squirrel chases the mouse.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("squirrel" "chases" "mouse" "-")
The mouse is young.
Unknown
rconc
[@1: The mouse is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "young" "+")
The cat does not eat the mouse.
Unknown
inv-rconc
[@3: The cat eats the mouse.[CWA. Example of deepest failure = (rule7 <- rule5 <- rule4 <- FAIL)]]
("cat" "eats" "mouse" "-")
The squirrel eats the mouse.
Unknown
rconc
[@3: The squirrel eats the mouse.[CWA. Example of deepest failure = (rule7 <- rule5 <- rule4 <- FAIL)]]
("squirrel" "eats" "mouse" "+")
The cat does not chase the mouse.
Unknown
inv-rconc
[@2: The cat chases the mouse.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("cat" "chases" "mouse" "-")
The squirrel is young.
Unknown
rconc
[@1: The squirrel is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "is" "young" "+")
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
The squirrel eats the rabbit.
Unknown
random
[@0: The squirrel eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "rabbit" "+")
The mouse is not cold.
Unknown
inv-random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
The cat does not chase the rabbit.
Unknown
inv-random
[@0: The cat chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "rabbit" "-")
The rabbit eats the squirrel.
Unknown
random
[@0: The rabbit eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "squirrel" "+")
@0: The cat is blue.[(triple1)] The mouse does not chase the squirrel.[(triple2)] The mouse eats the cat.[(triple3)] The mouse eats the rabbit.[(triple4)] The mouse is big.[(triple5)] The mouse sees the rabbit.[(triple6)] The mouse sees the squirrel.[(triple7)] The rabbit chases the squirrel.[(triple9)] The rabbit does not chase the cat.[(triple8)] The rabbit is young.[(triple10 OR ((triple9) -> rule2))] The squirrel eats the cat.[(triple11)] The squirrel sees the cat.[(triple12)] @1: The mouse is green.[(((triple7) -> rule4))] The rabbit sees the squirrel.[(((triple4) -> rule3))] @2: The mouse chases the mouse.[(((((triple7) -> rule4)) -> rule5))] The rabbit is green.[(((((triple4) -> rule3)) -> rule4))] @3: The mouse eats the mouse.[(((((((triple7) -> rule4)) -> rule5) triple3) -> rule7))] The rabbit chases the mouse.[(((((((triple4) -> rule3)) -> rule4)) -> rule5))] @4: The rabbit eats the mouse.[(((((((((triple4) -> rule3)) -> rule4)) -> rule5) triple3) -> rule7))] @5: The mouse does not chase the rabbit.[(((triple10 ((((((((triple4) -> rule3)) -> rule4)) -> rule5) triple3) -> rule7)) -> rule1) OR ((((triple9) -> rule2) ((((((((triple4) -> rule3)) -> rule4)) -> rule5) triple3) -> rule7)) -> rule1))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
The mouse does not chase the squirrel.
("mouse" "chases" "squirrel" "-")
triple2
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple3
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple4
The mouse is big.
("mouse" "is" "big" "+")
triple5
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple6
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple7
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
triple9
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
triple8
The rabbit is young.
("rabbit" "is" "young" "+")
triple10
((triple9) -> (rule2 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple11
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple12
The mouse is green.
("mouse" "is" "green" "+")
((triple7) -> (rule4 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
((triple4) -> (rule3 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((((triple7) -> (rule4 % int2))) -> (rule5 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((((((triple7) -> (rule4 % int3))) -> (rule5 % int2)) triple3) -> (rule7 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
((((((triple4) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int3
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
((((((((triple4) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule5 % int2)) triple3) -> (rule7 % int1))
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int4
The mouse does not chase the rabbit.
("mouse" "chases" "rabbit" "-")
((triple10 ((((((((triple4) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule5 % int3)) triple3) -> (rule7 % int2))) -> (rule1 % int1))
The mouse does not chase the rabbit.
("mouse" "chases" "rabbit" "-")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int3
The rabbit is green.
("rabbit" "is" "green" "+")
int4
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int5
((((triple9) -> (rule2 % int6)) ((((((((triple4) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule5 % int3)) triple3) -> (rule7 % int2))) -> (rule1 % int1))
The mouse does not chase the rabbit.
("mouse" "chases" "rabbit" "-")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int3
The rabbit is green.
("rabbit" "is" "green" "+")
int4
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int5
The rabbit is young.
("rabbit" "is" "young" "+")
int6