The cow is cold. The cow is kind. The cow is young. The cow likes the lion. The cow likes the squirrel. The lion eats the mouse. The lion sees the cow. The mouse eats the lion. The mouse likes the cow. The mouse likes the lion. The mouse likes the squirrel. The mouse sees the cow. The squirrel eats the mouse. The squirrel is rough. The squirrel is young. The squirrel likes the cow. All cold things are rough. If something sees the lion and it sees the mouse then the mouse is young. If something is rough and it eats the lion then the lion sees the mouse. If something sees the squirrel and it likes the lion then the squirrel eats the lion. Rough things are kind. If something is rough and it sees the cow then it sees the squirrel. If something eats the lion then it likes the squirrel. If something sees the cow then it is cold. If something eats the lion and the lion is kind then the lion is rough.
The cow is cold.
("cow" "is" "cold" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is young.
("cow" "is" "young" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
All cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If something sees the lion and it sees the mouse then the mouse is young.
((("something" "sees" "lion" "+") ("something" "sees" "mouse" "+")) -> ("mouse" "is" "young" "+"))
If something is rough and it eats the lion then the lion sees the mouse.
((("something" "is" "rough" "+") ("something" "eats" "lion" "+")) -> ("lion" "sees" "mouse" "+"))
If something sees the squirrel and it likes the lion then the squirrel eats the lion.
((("something" "sees" "squirrel" "+") ("something" "likes" "lion" "+")) -> ("squirrel" "eats" "lion" "+"))
Rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If something is rough and it sees the cow then it sees the squirrel.
((("something" "is" "rough" "+") ("something" "sees" "cow" "+")) -> ("something" "sees" "squirrel" "+"))
If something eats the lion then it likes the squirrel.
((("something" "eats" "lion" "+")) -> ("something" "likes" "squirrel" "+"))
If something sees the cow then it is cold.
((("something" "sees" "cow" "+")) -> ("something" "is" "cold" "+"))
If something eats the lion and the lion is kind then the lion is rough.
((("something" "eats" "lion" "+") ("lion" "is" "kind" "+")) -> ("lion" "is" "rough" "+"))
The lion eats the mouse.
True
1
proof
[(triple6)]
("lion" "eats" "mouse" "+")
triple6
The mouse does not like the squirrel.
False
1
inv-proof
[(triple11 OR ((triple8) -> rule7))]
("mouse" "likes" "squirrel" "-")
triple11
((triple8) -> (rule7 % int1))
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int1
The mouse is cold.
True
2
proof
[(((triple12) -> rule8))]
("mouse" "is" "cold" "+")
((triple12) -> (rule8 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is not cold.
False
2
inv-proof
[(((triple12) -> rule8))]
("mouse" "is" "cold" "-")
((triple12) -> (rule8 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is rough.
True
3
proof
[(((((triple12) -> rule8)) -> rule1))]
("mouse" "is" "rough" "+")
((((triple12) -> (rule8 % int2))) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The lion is not rough.
False
3
inv-proof
[(((((triple7) -> rule8)) -> rule1))]
("lion" "is" "rough" "-")
((((triple7) -> (rule8 % int2))) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is kind.
True
4
proof
[(((((((triple7) -> rule8)) -> rule1)) -> rule5))]
("lion" "is" "kind" "+")
((((((triple7) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The lion does not see the squirrel.
False
5
inv-proof
[(((((((triple7) -> rule8)) -> rule1) triple7) -> rule6))]
("lion" "sees" "squirrel" "-")
((((((triple7) -> (rule8 % int3))) -> (rule1 % int2)) triple7) -> (rule6 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The squirrel eats the lion.
True
7
proof
[(((((((((triple12) -> rule8)) -> rule1) triple12) -> rule6) triple10) -> rule4))]
("squirrel" "eats" "lion" "+")
((((((((triple12) -> (rule8 % int4))) -> (rule1 % int3)) triple12) -> (rule6 % int2)) triple10) -> (rule4 % int1))
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The mouse is cold.
("mouse" "is" "cold" "+")
int4
The squirrel does not eat the lion.
False
7
inv-proof
[(((((((((triple12) -> rule8)) -> rule1) triple12) -> rule6) triple10) -> rule4))]
("squirrel" "eats" "lion" "-")
((((((((triple12) -> (rule8 % int4))) -> (rule1 % int3)) triple12) -> (rule6 % int2)) triple10) -> (rule4 % int1))
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The mouse is cold.
("mouse" "is" "cold" "+")
int4
The squirrel likes the squirrel.
True
8
proof
[(((((((((((triple12) -> rule8)) -> rule1) triple12) -> rule6) triple10) -> rule4)) -> rule7))]
("squirrel" "likes" "squirrel" "+")
((((((((((triple12) -> (rule8 % int5))) -> (rule1 % int4)) triple12) -> (rule6 % int3)) triple10) -> (rule4 % int2))) -> (rule7 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int2
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
int4
The mouse is cold.
("mouse" "is" "cold" "+")
int5
The squirrel does not like the squirrel.
False
8
inv-proof
[(((((((((((triple12) -> rule8)) -> rule1) triple12) -> rule6) triple10) -> rule4)) -> rule7))]
("squirrel" "likes" "squirrel" "-")
((((((((((triple12) -> (rule8 % int5))) -> (rule1 % int4)) triple12) -> (rule6 % int3)) triple10) -> (rule4 % int2))) -> (rule7 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int2
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
int4
The mouse is cold.
("mouse" "is" "cold" "+")
int5
The mouse is not young.
Unknown
inv-rconc
[@1: The mouse is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "young" "-")
The squirrel is cold.
Unknown
rconc
[@1: The squirrel is cold.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "is" "cold" "+")
The cow does not see the squirrel.
Unknown
inv-rconc
[@1: The cow sees the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "sees" "squirrel" "-")
The squirrel sees the squirrel.
Unknown
rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "sees" "squirrel" "+")
The lion does not like the squirrel.
Unknown
inv-rconc
[@1: The lion likes the squirrel.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "likes" "squirrel" "-")
The cow likes the mouse.
Unknown
random
[@0: The cow likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "mouse" "+")
The cow does not eat the lion.
Unknown
inv-random
[@0: The cow eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "lion" "-")
The mouse eats the cow.
Unknown
random
[@0: The mouse eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "cow" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse eats the squirrel.
Unknown
random
[@0: The mouse eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "squirrel" "+")
The mouse is not big.
Unknown
inv-random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
@0: The cow is cold.[(triple1)] The cow is kind.[(triple2 OR ((((triple1) -> rule1)) -> rule5))] The cow is young.[(triple3)] The cow likes the lion.[(triple4)] The cow likes the squirrel.[(triple5)] The lion eats the mouse.[(triple6)] The lion sees the cow.[(triple7)] The mouse eats the lion.[(triple8)] The mouse likes the cow.[(triple9)] The mouse likes the lion.[(triple10)] The mouse likes the squirrel.[(triple11 OR ((triple8) -> rule7))] The mouse sees the cow.[(triple12)] The squirrel eats the mouse.[(triple13)] The squirrel is rough.[(triple14)] The squirrel is young.[(triple15)] The squirrel likes the cow.[(triple16)] @1: The cow is rough.[(((triple1) -> rule1))] The lion is cold.[(((triple7) -> rule8))] The mouse is cold.[(((triple12) -> rule8))] The squirrel is kind.[(((triple14) -> rule5))] @2: The lion is rough.[(((((triple7) -> rule8)) -> rule1))] The mouse is rough.[(((((triple12) -> rule8)) -> rule1))] @3: The lion is kind.[(((((((triple7) -> rule8)) -> rule1)) -> rule5))] The lion sees the mouse.[(((((((triple12) -> rule8)) -> rule1) triple8) -> rule3) OR ((triple14 ((((((((triple12) -> rule8)) -> rule1) triple12) -> rule6) triple10) -> rule4)) -> rule3))] The lion sees the squirrel.[(((((((triple7) -> rule8)) -> rule1) triple7) -> rule6))] The mouse is kind.[(((((((triple12) -> rule8)) -> rule1)) -> rule5))] The mouse sees the squirrel.[(((((((triple12) -> rule8)) -> rule1) triple12) -> rule6))] @4: The squirrel eats the lion.[(((((((((triple12) -> rule8)) -> rule1) triple12) -> rule6) triple10) -> rule4))] @5: The squirrel likes the squirrel.[(((((((((((triple12) -> rule8)) -> rule1) triple12) -> rule6) triple10) -> rule4)) -> rule7))]
The cow is cold.
("cow" "is" "cold" "+")
triple1
The cow is kind.
("cow" "is" "kind" "+")
triple2
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is young.
("cow" "is" "young" "+")
triple3
The cow likes the lion.
("cow" "likes" "lion" "+")
triple4
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
triple5
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple6
The lion sees the cow.
("lion" "sees" "cow" "+")
triple7
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple8
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple9
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple10
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple11
((triple8) -> (rule7 % int1))
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple12
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple13
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple14
The squirrel is young.
("squirrel" "is" "young" "+")
triple15
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
triple16
The cow is rough.
("cow" "is" "rough" "+")
((triple1) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
((triple7) -> (rule8 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
((triple12) -> (rule8 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
((triple14) -> (rule5 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
((((triple7) -> (rule8 % int2))) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
((((triple12) -> (rule8 % int2))) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
((((((triple7) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The lion sees the mouse.
("lion" "sees" "mouse" "+")
((((((triple12) -> (rule8 % int3))) -> (rule1 % int2)) triple8) -> (rule3 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
((triple14 ((((((((triple12) -> (rule8 % int5))) -> (rule1 % int4)) triple12) -> (rule6 % int3)) triple10) -> (rule4 % int2))) -> (rule3 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int2
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
int4
The mouse is cold.
("mouse" "is" "cold" "+")
int5
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
((((((triple7) -> (rule8 % int3))) -> (rule1 % int2)) triple7) -> (rule6 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
((((((triple12) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
((((((triple12) -> (rule8 % int3))) -> (rule1 % int2)) triple12) -> (rule6 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
((((((((triple12) -> (rule8 % int4))) -> (rule1 % int3)) triple12) -> (rule6 % int2)) triple10) -> (rule4 % int1))
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The mouse is cold.
("mouse" "is" "cold" "+")
int4
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((((((((((triple12) -> (rule8 % int5))) -> (rule1 % int4)) triple12) -> (rule6 % int3)) triple10) -> (rule4 % int2))) -> (rule7 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int2
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
int4
The mouse is cold.
("mouse" "is" "cold" "+")
int5