The cow is cold. The cow is nice. The cow sees the lion. The lion chases the cow. The lion eats the cow. The lion is cold. The mouse chases the cow. The mouse eats the lion. The mouse is big. The mouse is cold. The mouse sees the cow. The squirrel chases the mouse. The squirrel is cold. The squirrel is nice. The squirrel sees the lion. If someone sees the squirrel and the squirrel sees the lion then the lion is big. If someone is nice then they see the squirrel. If someone is big and cold then they see the squirrel. If the mouse is cold and the mouse is green then the mouse chases the cow. All young people are green. If the mouse sees the lion then the lion is nice.
The cow is cold.
("cow" "is" "cold" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion eats the cow.
("lion" "eats" "cow" "+")
The lion is cold.
("lion" "is" "cold" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
If someone sees the squirrel and the squirrel sees the lion then the lion is big.
((("someone" "sees" "squirrel" "+") ("squirrel" "sees" "lion" "+")) -> ("lion" "is" "big" "+"))
If someone is nice then they see the squirrel.
((("someone" "is" "nice" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone is big and cold then they see the squirrel.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "sees" "squirrel" "+"))
If the mouse is cold and the mouse is green then the mouse chases the cow.
((("mouse" "is" "cold" "+") ("mouse" "is" "green" "+")) -> ("mouse" "chases" "cow" "+"))
All young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
If the mouse sees the lion then the lion is nice.
((("mouse" "sees" "lion" "+")) -> ("lion" "is" "nice" "+"))
The squirrel sees the lion.
True
1
proof
[(triple15)]
("squirrel" "sees" "lion" "+")
triple15
The mouse is not cold.
False
1
inv-proof
[(triple10)]
("mouse" "is" "cold" "-")
triple10
The cow sees the squirrel.
True
2
proof
[(((triple2) -> rule2))]
("cow" "sees" "squirrel" "+")
((triple2) -> (rule2 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The mouse does not see the squirrel.
False
3
inv-proof
[(((triple9 triple10) -> rule3))]
("mouse" "sees" "squirrel" "-")
((triple9 triple10) -> (rule3 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The lion is big.
True
4
proof
[(((((triple14) -> rule2) triple15) -> rule1) OR ((((triple2) -> rule2) triple15) -> rule1) OR ((((triple9 triple10) -> rule3) triple15) -> rule1))]
("lion" "is" "big" "+")
((((triple14) -> (rule2 % int2)) triple15) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
((((triple2) -> (rule2 % int2)) triple15) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int2
((((triple9 triple10) -> (rule3 % int2)) triple15) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The lion is not big.
False
4
inv-proof
[(((((triple14) -> rule2) triple15) -> rule1) OR ((((triple2) -> rule2) triple15) -> rule1) OR ((((triple9 triple10) -> rule3) triple15) -> rule1))]
("lion" "is" "big" "-")
((((triple14) -> (rule2 % int2)) triple15) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
((((triple2) -> (rule2 % int2)) triple15) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int2
((((triple9 triple10) -> (rule3 % int2)) triple15) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The lion sees the squirrel.
True
6
proof
[(((((((triple14) -> rule2) triple15) -> rule1) triple6) -> rule3) OR ((((((triple2) -> rule2) triple15) -> rule1) triple6) -> rule3) OR ((((((triple9 triple10) -> rule3) triple15) -> rule1) triple6) -> rule3))]
("lion" "sees" "squirrel" "+")
((((((triple14) -> (rule2 % int3)) triple15) -> (rule1 % int2)) triple6) -> (rule3 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int3
((((((triple2) -> (rule2 % int3)) triple15) -> (rule1 % int2)) triple6) -> (rule3 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int3
((((((triple9 triple10) -> (rule3 % int3)) triple15) -> (rule1 % int2)) triple6) -> (rule3 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int3
The lion does not see the squirrel.
False
6
inv-proof
[(((((((triple14) -> rule2) triple15) -> rule1) triple6) -> rule3) OR ((((((triple2) -> rule2) triple15) -> rule1) triple6) -> rule3) OR ((((((triple9 triple10) -> rule3) triple15) -> rule1) triple6) -> rule3))]
("lion" "sees" "squirrel" "-")
((((((triple14) -> (rule2 % int3)) triple15) -> (rule1 % int2)) triple6) -> (rule3 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int3
((((((triple2) -> (rule2 % int3)) triple15) -> (rule1 % int2)) triple6) -> (rule3 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int3
((((((triple9 triple10) -> (rule3 % int3)) triple15) -> (rule1 % int2)) triple6) -> (rule3 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int3
The lion is not nice.
Unknown
inv-rconc
[@1: The lion is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "is" "nice" "-")
The squirrel is green.
Unknown
rconc
[@1: The squirrel is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "is" "green" "+")
The lion is not green.
Unknown
inv-rconc
[@1: The lion is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "is" "green" "-")
The mouse is green.
Unknown
rconc
[@1: The mouse is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "green" "+")
The lion does not eat the squirrel.
Unknown
inv-random
[@0: The lion eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "squirrel" "-")
The squirrel eats the mouse.
Unknown
random
[@0: The squirrel eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "mouse" "+")
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The cow chases the lion.
Unknown
random
[@0: The cow chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "lion" "+")
@0: The cow is cold.[(triple1)] The cow is nice.[(triple2)] The cow sees the lion.[(triple3)] The lion chases the cow.[(triple4)] The lion eats the cow.[(triple5)] The lion is cold.[(triple6)] The mouse chases the cow.[(triple7)] The mouse eats the lion.[(triple8)] The mouse is big.[(triple9)] The mouse is cold.[(triple10)] The mouse sees the cow.[(triple11)] The squirrel chases the mouse.[(triple12)] The squirrel is cold.[(triple13)] The squirrel is nice.[(triple14)] The squirrel sees the lion.[(triple15)] @1: The cow sees the squirrel.[(((triple2) -> rule2))] The mouse sees the squirrel.[(((triple9 triple10) -> rule3))] The squirrel sees the squirrel.[(((triple14) -> rule2))] @2: The lion is big.[(((((triple14) -> rule2) triple15) -> rule1) OR ((((triple2) -> rule2) triple15) -> rule1) OR ((((triple9 triple10) -> rule3) triple15) -> rule1))] @3: The lion sees the squirrel.[(((((((triple14) -> rule2) triple15) -> rule1) triple6) -> rule3) OR ((((((triple2) -> rule2) triple15) -> rule1) triple6) -> rule3) OR ((((((triple9 triple10) -> rule3) triple15) -> rule1) triple6) -> rule3))]
The cow is cold.
("cow" "is" "cold" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
triple2
The cow sees the lion.
("cow" "sees" "lion" "+")
triple3
The lion chases the cow.
("lion" "chases" "cow" "+")
triple4
The lion eats the cow.
("lion" "eats" "cow" "+")
triple5
The lion is cold.
("lion" "is" "cold" "+")
triple6
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple7
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple8
The mouse is big.
("mouse" "is" "big" "+")
triple9
The mouse is cold.
("mouse" "is" "cold" "+")
triple10
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple11
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
triple12
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple13
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple14
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple15
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
((triple2) -> (rule2 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
((triple9 triple10) -> (rule3 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((triple14) -> (rule2 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The lion is big.
("lion" "is" "big" "+")
((((triple14) -> (rule2 % int2)) triple15) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
((((triple2) -> (rule2 % int2)) triple15) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int2
((((triple9 triple10) -> (rule3 % int2)) triple15) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
((((((triple14) -> (rule2 % int3)) triple15) -> (rule1 % int2)) triple6) -> (rule3 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int3
((((((triple2) -> (rule2 % int3)) triple15) -> (rule1 % int2)) triple6) -> (rule3 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int3
((((((triple9 triple10) -> (rule3 % int3)) triple15) -> (rule1 % int2)) triple6) -> (rule3 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int3