The cat eats the lion. The cat eats the mouse. The cat is rough. The cat is young. The cat needs the lion. The cat needs the mouse. The lion eats the cat. The lion eats the mouse. The lion is blue. The lion is rough. The lion needs the cat. The lion sees the cat. The mouse eats the cat. The mouse is kind. The mouse needs the lion. The mouse sees the cat. If someone sees the cat and they see the mouse then the mouse sees the lion. If someone eats the mouse and they eat the lion then the lion is blue. If the cat sees the lion then the lion sees the cat. If the lion sees the cat then the cat is kind. If someone is rough then they see the lion. If someone eats the mouse then they see the mouse.
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is young.
("cat" "is" "young" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
If someone sees the cat and they see the mouse then the mouse sees the lion.
((("someone" "sees" "cat" "+") ("someone" "sees" "mouse" "+")) -> ("mouse" "sees" "lion" "+"))
If someone eats the mouse and they eat the lion then the lion is blue.
((("someone" "eats" "mouse" "+") ("someone" "eats" "lion" "+")) -> ("lion" "is" "blue" "+"))
If the cat sees the lion then the lion sees the cat.
((("cat" "sees" "lion" "+")) -> ("lion" "sees" "cat" "+"))
If the lion sees the cat then the cat is kind.
((("lion" "sees" "cat" "+")) -> ("cat" "is" "kind" "+"))
If someone is rough then they see the lion.
((("someone" "is" "rough" "+")) -> ("someone" "sees" "lion" "+"))
If someone eats the mouse then they see the mouse.
((("someone" "eats" "mouse" "+")) -> ("someone" "sees" "mouse" "+"))
The mouse needs the lion.
True
1
proof
[(triple15)]
("mouse" "needs" "lion" "+")
triple15
The lion does not need the cat.
False
1
inv-proof
[(triple11)]
("lion" "needs" "cat" "-")
triple11
The cat sees the mouse.
True
2
proof
[(((triple2) -> rule6))]
("cat" "sees" "mouse" "+")
((triple2) -> (rule6 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat is not kind.
False
2
inv-proof
[(((triple12) -> rule4) OR ((((((triple3) -> rule5)) -> rule3)) -> rule4))]
("cat" "is" "kind" "-")
((triple12) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The cat sees the lion.
("cat" "sees" "lion" "+")
int3
The mouse sees the lion.
True
4
proof
[(((triple12 ((triple8) -> rule6)) -> rule1) OR ((((((triple3) -> rule5)) -> rule3) ((triple8) -> rule6)) -> rule1))]
("mouse" "sees" "lion" "+")
((triple12 ((triple8) -> (rule6 % int2))) -> (rule1 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
((((((triple3) -> (rule5 % int4))) -> (rule3 % int3)) ((triple8) -> (rule6 % int2))) -> (rule1 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
int3
The cat sees the lion.
("cat" "sees" "lion" "+")
int4
The mouse does not see the lion.
False
4
inv-proof
[(((triple12 ((triple8) -> rule6)) -> rule1) OR ((((((triple3) -> rule5)) -> rule3) ((triple8) -> rule6)) -> rule1))]
("mouse" "sees" "lion" "-")
((triple12 ((triple8) -> (rule6 % int2))) -> (rule1 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
((((((triple3) -> (rule5 % int4))) -> (rule3 % int3)) ((triple8) -> (rule6 % int2))) -> (rule1 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
int3
The cat sees the lion.
("cat" "sees" "lion" "+")
int4
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
The mouse does not eat the lion.
Unknown
inv-random
[@0: The mouse eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "lion" "-")
The mouse needs the cat.
Unknown
random
[@0: The mouse needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "cat" "+")
The mouse is not blue.
Unknown
inv-random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
@0: The cat eats the lion.[(triple1)] The cat eats the mouse.[(triple2)] The cat is rough.[(triple3)] The cat is young.[(triple4)] The cat needs the lion.[(triple5)] The cat needs the mouse.[(triple6)] The lion eats the cat.[(triple7)] The lion eats the mouse.[(triple8)] The lion is blue.[(triple9 OR ((triple2 triple1) -> rule2))] The lion is rough.[(triple10)] The lion needs the cat.[(triple11)] The lion sees the cat.[(triple12 OR ((((triple3) -> rule5)) -> rule3))] The mouse eats the cat.[(triple13)] The mouse is kind.[(triple14)] The mouse needs the lion.[(triple15)] The mouse sees the cat.[(triple16)] @1: The cat is kind.[(((triple12) -> rule4) OR ((((((triple3) -> rule5)) -> rule3)) -> rule4))] The cat sees the lion.[(((triple3) -> rule5))] The cat sees the mouse.[(((triple2) -> rule6))] The lion sees the lion.[(((triple10) -> rule5))] The lion sees the mouse.[(((triple8) -> rule6))] @2: The mouse sees the lion.[(((triple12 ((triple8) -> rule6)) -> rule1) OR ((((((triple3) -> rule5)) -> rule3) ((triple8) -> rule6)) -> rule1))]
The cat eats the lion.
("cat" "eats" "lion" "+")
triple1
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple2
The cat is rough.
("cat" "is" "rough" "+")
triple3
The cat is young.
("cat" "is" "young" "+")
triple4
The cat needs the lion.
("cat" "needs" "lion" "+")
triple5
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple6
The lion eats the cat.
("lion" "eats" "cat" "+")
triple7
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple8
The lion is blue.
("lion" "is" "blue" "+")
triple9
((triple2 triple1) -> (rule2 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
triple10
The lion needs the cat.
("lion" "needs" "cat" "+")
triple11
The lion sees the cat.
("lion" "sees" "cat" "+")
triple12
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The cat sees the lion.
("cat" "sees" "lion" "+")
int2
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple13
The mouse is kind.
("mouse" "is" "kind" "+")
triple14
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple15
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple16
The cat is kind.
("cat" "is" "kind" "+")
((triple12) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The cat sees the lion.
("cat" "sees" "lion" "+")
int3
The cat sees the lion.
("cat" "sees" "lion" "+")
((triple3) -> (rule5 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
((triple2) -> (rule6 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
((triple10) -> (rule5 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
((triple8) -> (rule6 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
((triple12 ((triple8) -> (rule6 % int2))) -> (rule1 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
((((((triple3) -> (rule5 % int4))) -> (rule3 % int3)) ((triple8) -> (rule6 % int2))) -> (rule1 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
int3
The cat sees the lion.
("cat" "sees" "lion" "+")
int4