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