The lion chases the mouse. The lion is green. The lion is kind. The lion sees the tiger. The mouse chases the lion. The mouse is big. The mouse is green. The mouse is kind. The mouse is rough. The mouse likes the lion. The mouse likes the tiger. The tiger is big. The tiger is red. The tiger likes the lion. The tiger likes the mouse. If something is green then it chases the mouse. If something chases the tiger then it likes the lion. If something chases the lion then it is green. If something is kind and it sees the tiger then the tiger chases the lion. If something sees the lion and the lion sees the mouse then the mouse chases the lion. If something chases the mouse and it is big then the mouse sees the tiger.
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
If something is green then it chases the mouse.
((("something" "is" "green" "+")) -> ("something" "chases" "mouse" "+"))
If something chases the tiger then it likes the lion.
((("something" "chases" "tiger" "+")) -> ("something" "likes" "lion" "+"))
If something chases the lion then it is green.
((("something" "chases" "lion" "+")) -> ("something" "is" "green" "+"))
If something is kind and it sees the tiger then the tiger chases the lion.
((("something" "is" "kind" "+") ("something" "sees" "tiger" "+")) -> ("tiger" "chases" "lion" "+"))
If something sees the lion and the lion sees the mouse then the mouse chases the lion.
((("something" "sees" "lion" "+") ("lion" "sees" "mouse" "+")) -> ("mouse" "chases" "lion" "+"))
If something chases the mouse and it is big then the mouse sees the tiger.
((("something" "chases" "mouse" "+") ("something" "is" "big" "+")) -> ("mouse" "sees" "tiger" "+"))
The mouse is kind.
True
1
proof
[(triple8)]
("mouse" "is" "kind" "+")
triple8
The tiger does not like the mouse.
False
1
inv-proof
[(triple15)]
("tiger" "likes" "mouse" "-")
triple15
The mouse chases the mouse.
True
2
proof
[(((triple7) -> rule1) OR ((((triple5) -> rule3)) -> rule1))]
("mouse" "chases" "mouse" "+")
((triple7) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule1 % 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
2
inv-proof
[(((triple7) -> rule1) OR ((((triple5) -> rule3)) -> rule1))]
("mouse" "chases" "mouse" "-")
((triple7) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse sees the tiger.
True
4
proof
[(((((triple7) -> rule1) triple6) -> rule6) OR ((((((triple5) -> rule3)) -> rule1) triple6) -> rule6) OR ((((((((triple3 triple4) -> rule4)) -> rule3)) -> rule1) triple12) -> rule6))]
("mouse" "sees" "tiger" "+")
((((triple7) -> (rule1 % int2)) triple6) -> (rule6 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
((((((triple5) -> (rule3 % int3))) -> (rule1 % int2)) triple6) -> (rule6 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
((((((((triple3 triple4) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule1 % int2)) triple12) -> (rule6 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int4
The tiger is not green.
False
4
inv-proof
[(((((triple3 triple4) -> rule4)) -> rule3) OR ((((triple8 ((((triple7) -> rule1) triple6) -> rule6)) -> rule4)) -> rule3) OR ((((triple8 ((((((triple5) -> rule3)) -> rule1) triple6) -> rule6)) -> rule4)) -> rule3))]
("tiger" "is" "green" "-")
((((triple3 triple4) -> (rule4 % int2))) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int2
((((triple8 ((((triple7) -> (rule1 % int4)) triple6) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int3
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int4
((((triple8 ((((((triple5) -> (rule3 % int5))) -> (rule1 % int4)) triple6) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int3
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int4
The mouse is green.
("mouse" "is" "green" "+")
int5
The tiger chases the mouse.
True
5
proof
[(((((((triple3 triple4) -> rule4)) -> rule3)) -> rule1) OR ((((((triple8 ((((triple7) -> rule1) triple6) -> rule6)) -> rule4)) -> rule3)) -> rule1) OR ((((((triple8 ((((((triple5) -> rule3)) -> rule1) triple6) -> rule6)) -> rule4)) -> rule3)) -> rule1))]
("tiger" "chases" "mouse" "+")
((((((triple3 triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int3
((((((triple8 ((((triple7) -> (rule1 % int5)) triple6) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int4
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int5
((((((triple8 ((((((triple5) -> (rule3 % int6))) -> (rule1 % int5)) triple6) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int4
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int5
The mouse is green.
("mouse" "is" "green" "+")
int6
The tiger does not chase the mouse.
False
5
inv-proof
[(((((((triple3 triple4) -> rule4)) -> rule3)) -> rule1) OR ((((((triple8 ((((triple7) -> rule1) triple6) -> rule6)) -> rule4)) -> rule3)) -> rule1) OR ((((((triple8 ((((((triple5) -> rule3)) -> rule1) triple6) -> rule6)) -> rule4)) -> rule3)) -> rule1))]
("tiger" "chases" "mouse" "-")
((((((triple3 triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int3
((((((triple8 ((((triple7) -> (rule1 % int5)) triple6) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int4
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int5
((((((triple8 ((((((triple5) -> (rule3 % int6))) -> (rule1 % int5)) triple6) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int4
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int5
The mouse is green.
("mouse" "is" "green" "+")
int6
The lion does not like the lion.
Unknown
inv-rconc
[@1: The lion likes the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "likes" "lion" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
The lion is not rough.
Unknown
inv-random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "-")
The lion likes the tiger.
Unknown
random
[@0: The lion likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "tiger" "+")
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The lion chases the mouse.[(triple1 OR ((triple2) -> rule1))] The lion is green.[(triple2)] The lion is kind.[(triple3)] The lion sees the tiger.[(triple4)] The mouse chases the lion.[(triple5)] The mouse is big.[(triple6)] The mouse is green.[(triple7 OR ((triple5) -> rule3))] The mouse is kind.[(triple8)] The mouse is rough.[(triple9)] The mouse likes the lion.[(triple10)] The mouse likes the tiger.[(triple11)] The tiger is big.[(triple12)] The tiger is red.[(triple13)] The tiger likes the lion.[(triple14)] The tiger likes the mouse.[(triple15)] @1: The mouse chases the mouse.[(((triple7) -> rule1) OR ((((triple5) -> rule3)) -> rule1))] The tiger chases the lion.[(((triple3 triple4) -> rule4) OR ((triple8 ((((triple7) -> rule1) triple6) -> rule6)) -> rule4) OR ((triple8 ((((((triple5) -> rule3)) -> rule1) triple6) -> rule6)) -> rule4))] @2: The mouse sees the tiger.[(((((triple7) -> rule1) triple6) -> rule6) OR ((((((triple5) -> rule3)) -> rule1) triple6) -> rule6) OR ((((((((triple3 triple4) -> rule4)) -> rule3)) -> rule1) triple12) -> rule6))] The tiger is green.[(((((triple3 triple4) -> rule4)) -> rule3) OR ((((triple8 ((((triple7) -> rule1) triple6) -> rule6)) -> rule4)) -> rule3) OR ((((triple8 ((((((triple5) -> rule3)) -> rule1) triple6) -> rule6)) -> rule4)) -> rule3))] @3: The tiger chases the mouse.[(((((((triple3 triple4) -> rule4)) -> rule3)) -> rule1) OR ((((((triple8 ((((triple7) -> rule1) triple6) -> rule6)) -> rule4)) -> rule3)) -> rule1) OR ((((((triple8 ((((((triple5) -> rule3)) -> rule1) triple6) -> rule6)) -> rule4)) -> rule3)) -> rule1))]
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple1
((triple2) -> (rule1 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion is green.
("lion" "is" "green" "+")
triple2
The lion is kind.
("lion" "is" "kind" "+")
triple3
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple4
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple5
The mouse is big.
("mouse" "is" "big" "+")
triple6
The mouse is green.
("mouse" "is" "green" "+")
triple7
((triple5) -> (rule3 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
triple8
The mouse is rough.
("mouse" "is" "rough" "+")
triple9
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple10
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple11
The tiger is big.
("tiger" "is" "big" "+")
triple12
The tiger is red.
("tiger" "is" "red" "+")
triple13
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple14
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple15
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((triple7) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The tiger chases the lion.
("tiger" "chases" "lion" "+")
((triple3 triple4) -> (rule4 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
((triple8 ((((triple7) -> (rule1 % int3)) triple6) -> (rule6 % int2))) -> (rule4 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int3
((triple8 ((((((triple5) -> (rule3 % int4))) -> (rule1 % int3)) triple6) -> (rule6 % int2))) -> (rule4 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int3
The mouse is green.
("mouse" "is" "green" "+")
int4
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
((((triple7) -> (rule1 % int2)) triple6) -> (rule6 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
((((((triple5) -> (rule3 % int3))) -> (rule1 % int2)) triple6) -> (rule6 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
((((((((triple3 triple4) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule1 % int2)) triple12) -> (rule6 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int4
The tiger is green.
("tiger" "is" "green" "+")
((((triple3 triple4) -> (rule4 % int2))) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int2
((((triple8 ((((triple7) -> (rule1 % int4)) triple6) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int3
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int4
((((triple8 ((((((triple5) -> (rule3 % int5))) -> (rule1 % int4)) triple6) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int3
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int4
The mouse is green.
("mouse" "is" "green" "+")
int5
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
((((((triple3 triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int3
((((((triple8 ((((triple7) -> (rule1 % int5)) triple6) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int4
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int5
((((((triple8 ((((((triple5) -> (rule3 % int6))) -> (rule1 % int5)) triple6) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int4
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int5
The mouse is green.
("mouse" "is" "green" "+")
int6