The bear does not chase the mouse. The bear chases the squirrel. The bear is cold. The bear is green. The bear is kind. The bear is round. The bear needs the squirrel. The bear visits the mouse. The bear visits the squirrel. The lion chases the bear. The lion chases the squirrel. The lion is green. The mouse chases the squirrel. The mouse does not visit the squirrel. The squirrel needs the lion. The squirrel visits the mouse. If someone chases the squirrel then they chase the bear. If someone chases the squirrel and the squirrel visits the lion then the squirrel does not visit the mouse. If someone needs the mouse then they are cold. If someone needs the bear then the bear chases the lion. If the lion chases the squirrel and the squirrel visits the mouse then the mouse needs the bear. If someone chases the lion then the lion needs the mouse. If someone is cold then they visit the squirrel.
The bear does not chase the mouse.
("bear" "chases" "mouse" "-")
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is green.
("bear" "is" "green" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear is round.
("bear" "is" "round" "+")
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
The lion chases the bear.
("lion" "chases" "bear" "+")
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The lion is green.
("lion" "is" "green" "+")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse does not visit the squirrel.
("mouse" "visits" "squirrel" "-")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If someone chases the squirrel then they chase the bear.
((("someone" "chases" "squirrel" "+")) -> ("someone" "chases" "bear" "+"))
If someone chases the squirrel and the squirrel visits the lion then the squirrel does not visit the mouse.
((("someone" "chases" "squirrel" "+") ("squirrel" "visits" "lion" "+")) -> ("squirrel" "visits" "mouse" "-"))
If someone needs the mouse then they are cold.
((("someone" "needs" "mouse" "+")) -> ("someone" "is" "cold" "+"))
If someone needs the bear then the bear chases the lion.
((("someone" "needs" "bear" "+")) -> ("bear" "chases" "lion" "+"))
If the lion chases the squirrel and the squirrel visits the mouse then the mouse needs the bear.
((("lion" "chases" "squirrel" "+") ("squirrel" "visits" "mouse" "+")) -> ("mouse" "needs" "bear" "+"))
If someone chases the lion then the lion needs the mouse.
((("someone" "chases" "lion" "+")) -> ("lion" "needs" "mouse" "+"))
If someone is cold then they visit the squirrel.
((("someone" "is" "cold" "+")) -> ("someone" "visits" "squirrel" "+"))
The bear is round.
True
1
proof
[(triple6)]
("bear" "is" "round" "+")
triple6
The lion does not chase the squirrel.
False
1
inv-proof
[(triple11)]
("lion" "chases" "squirrel" "-")
triple11
The bear chases the bear.
True
2
proof
[(((triple2) -> rule1))]
("bear" "chases" "bear" "+")
((triple2) -> (rule1 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The mouse does not need the bear.
False
3
inv-proof
[(((triple11 triple16) -> rule5))]
("mouse" "needs" "bear" "-")
((triple11 triple16) -> (rule5 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The bear chases the lion.
True
4
proof
[(((((triple11 triple16) -> rule5)) -> rule4))]
("bear" "chases" "lion" "+")
((((triple11 triple16) -> (rule5 % int2))) -> (rule4 % int1))
The bear chases the lion.
("bear" "chases" "lion" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The bear does not chase the lion.
False
4
inv-proof
[(((((triple11 triple16) -> rule5)) -> rule4))]
("bear" "chases" "lion" "-")
((((triple11 triple16) -> (rule5 % int2))) -> (rule4 % int1))
The bear chases the lion.
("bear" "chases" "lion" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The lion needs the mouse.
True
5
proof
[(((((((triple11 triple16) -> rule5)) -> rule4)) -> rule6))]
("lion" "needs" "mouse" "+")
((((((triple11 triple16) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The bear chases the lion.
("bear" "chases" "lion" "+")
int2
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int3
The lion does not need the mouse.
False
5
inv-proof
[(((((((triple11 triple16) -> rule5)) -> rule4)) -> rule6))]
("lion" "needs" "mouse" "-")
((((((triple11 triple16) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The bear chases the lion.
("bear" "chases" "lion" "+")
int2
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int3
The lion is cold.
True
6
proof
[(((((((((triple11 triple16) -> rule5)) -> rule4)) -> rule6)) -> rule3))]
("lion" "is" "cold" "+")
((((((((triple11 triple16) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int2
The bear chases the lion.
("bear" "chases" "lion" "+")
int3
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int4
The lion is not cold.
False
6
inv-proof
[(((((((((triple11 triple16) -> rule5)) -> rule4)) -> rule6)) -> rule3))]
("lion" "is" "cold" "-")
((((((((triple11 triple16) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int2
The bear chases the lion.
("bear" "chases" "lion" "+")
int3
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int4
The lion visits the squirrel.
True
7
proof
[(((((((((((triple11 triple16) -> rule5)) -> rule4)) -> rule6)) -> rule3)) -> rule7))]
("lion" "visits" "squirrel" "+")
((((((((((triple11 triple16) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int3
The bear chases the lion.
("bear" "chases" "lion" "+")
int4
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int5
The lion does not visit the squirrel.
False
7
inv-proof
[(((((((((((triple11 triple16) -> rule5)) -> rule4)) -> rule6)) -> rule3)) -> rule7))]
("lion" "visits" "squirrel" "-")
((((((((((triple11 triple16) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int3
The bear chases the lion.
("bear" "chases" "lion" "+")
int4
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int5
The squirrel does not visit the squirrel.
Unknown
inv-rconc
[@2: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("squirrel" "visits" "squirrel" "-")
The squirrel is cold.
Unknown
rconc
[@1: The squirrel is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "cold" "+")
The squirrel does not chase the bear.
Unknown
inv-rconc
[@1: The squirrel chases the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "chases" "bear" "-")
The mouse is cold.
Unknown
rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "cold" "+")
The mouse does not visit the bear.
Unknown
inv-random
[@0: The mouse visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "bear" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
The squirrel does not visit the bear.
Unknown
inv-random
[@0: The squirrel visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "bear" "-")
The lion is big.
Unknown
random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "+")
The mouse does not need the squirrel.
Unknown
inv-random
[@0: The mouse needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "squirrel" "-")
The bear visits the lion.
Unknown
random
[@0: The bear visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "lion" "+")
The lion does not chase the mouse.
Unknown
inv-random
[@0: The lion chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "mouse" "-")
The squirrel needs the bear.
Unknown
random
[@0: The squirrel needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "bear" "+")
@0: The bear chases the squirrel.[(triple2)] The bear does not chase the mouse.[(triple1)] The bear is cold.[(triple3)] The bear is green.[(triple4)] The bear is kind.[(triple5)] The bear is round.[(triple6)] The bear needs the squirrel.[(triple7)] The bear visits the mouse.[(triple8)] The bear visits the squirrel.[(triple9 OR ((triple3) -> rule7))] The lion chases the bear.[(triple10 OR ((triple11) -> rule1))] The lion chases the squirrel.[(triple11)] The lion is green.[(triple12)] The mouse chases the squirrel.[(triple13)] The mouse does not visit the squirrel.[(triple14)] The squirrel needs the lion.[(triple15)] The squirrel visits the mouse.[(triple16)] @1: The bear chases the bear.[(((triple2) -> rule1))] The mouse chases the bear.[(((triple13) -> rule1))] The mouse needs the bear.[(((triple11 triple16) -> rule5))] @2: The bear chases the lion.[(((((triple11 triple16) -> rule5)) -> rule4))] @3: The lion needs the mouse.[(((((((triple11 triple16) -> rule5)) -> rule4)) -> rule6))] @4: The lion is cold.[(((((((((triple11 triple16) -> rule5)) -> rule4)) -> rule6)) -> rule3))] @5: The lion visits the squirrel.[(((((((((((triple11 triple16) -> rule5)) -> rule4)) -> rule6)) -> rule3)) -> rule7))]
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple2
The bear does not chase the mouse.
("bear" "chases" "mouse" "-")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple3
The bear is green.
("bear" "is" "green" "+")
triple4
The bear is kind.
("bear" "is" "kind" "+")
triple5
The bear is round.
("bear" "is" "round" "+")
triple6
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
triple7
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple8
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
triple9
((triple3) -> (rule7 % int1))
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int1
The lion chases the bear.
("lion" "chases" "bear" "+")
triple10
((triple11) -> (rule1 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple11
The lion is green.
("lion" "is" "green" "+")
triple12
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple13
The mouse does not visit the squirrel.
("mouse" "visits" "squirrel" "-")
triple14
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple15
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple16
The bear chases the bear.
("bear" "chases" "bear" "+")
((triple2) -> (rule1 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The mouse chases the bear.
("mouse" "chases" "bear" "+")
((triple13) -> (rule1 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
((triple11 triple16) -> (rule5 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The bear chases the lion.
("bear" "chases" "lion" "+")
((((triple11 triple16) -> (rule5 % int2))) -> (rule4 % int1))
The bear chases the lion.
("bear" "chases" "lion" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
((((((triple11 triple16) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The bear chases the lion.
("bear" "chases" "lion" "+")
int2
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int3
The lion is cold.
("lion" "is" "cold" "+")
((((((((triple11 triple16) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int2
The bear chases the lion.
("bear" "chases" "lion" "+")
int3
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int4
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
((((((((((triple11 triple16) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int3
The bear chases the lion.
("bear" "chases" "lion" "+")
int4
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int5