The cat is red. The cat is not round. The cat needs the lion. The cat sees the lion. The cat visits the lion. The lion is not round. The lion needs the mouse. The mouse is rough. The mouse is round. The mouse needs the lion. The mouse needs the rabbit. The mouse visits the cat. The mouse visits the lion. The mouse visits the rabbit. The rabbit does not see the lion. The rabbit visits the mouse. If someone sees the cat then they are not red. If someone is nice and not young then they are not red. If someone needs the lion then they visit the cat. If someone sees the rabbit then they do not visit the cat. If the rabbit needs the lion and the lion is nice then the rabbit is not nice. If someone sees the cat and they are round then the cat needs the rabbit. If someone is round and they do not see the mouse then the mouse is not rough. If the cat needs the rabbit then the rabbit is round. If someone is round then they see the cat.
The cat is red.
("cat" "is" "red" "+")
The cat is not round.
("cat" "is" "round" "-")
The cat needs the lion.
("cat" "needs" "lion" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The lion is not round.
("lion" "is" "round" "-")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit does not see the lion.
("rabbit" "sees" "lion" "-")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If someone sees the cat then they are not red.
((("someone" "sees" "cat" "+")) -> ("someone" "is" "red" "-"))
If someone is nice and not young then they are not red.
((("someone" "is" "nice" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "red" "-"))
If someone needs the lion then they visit the cat.
((("someone" "needs" "lion" "+")) -> ("someone" "visits" "cat" "+"))
If someone sees the rabbit then they do not visit the cat.
((("someone" "sees" "rabbit" "+")) -> ("someone" "visits" "cat" "-"))
If the rabbit needs the lion and the lion is nice then the rabbit is not nice.
((("rabbit" "needs" "lion" "+") ("lion" "is" "nice" "+")) -> ("rabbit" "is" "nice" "-"))
If someone sees the cat and they are round then the cat needs the rabbit.
((("someone" "sees" "cat" "+") ("someone" "is" "round" "+")) -> ("cat" "needs" "rabbit" "+"))
If someone is round and they do not see the mouse then the mouse is not rough.
((("someone" "is" "round" "+") ("someone" "sees" "mouse" "~")) -> ("mouse" "is" "rough" "-"))
If the cat needs the rabbit then the rabbit is round.
((("cat" "needs" "rabbit" "+")) -> ("rabbit" "is" "round" "+"))
If someone is round then they see the cat.
((("someone" "is" "round" "+")) -> ("someone" "sees" "cat" "+"))
The mouse is round.
True
1
proof
[(triple9)]
("mouse" "is" "round" "+")
triple9
The mouse is not round.
False
1
inv-proof
[(triple9)]
("mouse" "is" "round" "-")
triple9
The cat visits the cat.
True
2
proof
[(((triple3) -> rule3))]
("cat" "visits" "cat" "+")
((triple3) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat does not visit the cat.
False
2
inv-proof
[(((triple3) -> rule3))]
("cat" "visits" "cat" "-")
((triple3) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat needs the rabbit.
True
4
proof
[(((((triple9) -> rule9) triple9) -> rule6))]
("cat" "needs" "rabbit" "+")
((((triple9) -> (rule9 % int2)) triple9) -> (rule6 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The mouse is red.
False
3
inv-proof
[(((((triple9) -> rule9)) -> rule1))]
("mouse" "is" "red" "+")
((((triple9) -> (rule9 % int2))) -> (rule1 % int1))
The mouse is not red.
("mouse" "is" "red" "-")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The rabbit is round.
True
5
proof
[(((((((triple9) -> rule9) triple9) -> rule6)) -> rule8))]
("rabbit" "is" "round" "+")
((((((triple9) -> (rule9 % int3)) triple9) -> (rule6 % int2))) -> (rule8 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int3
The rabbit is not round.
False
5
inv-proof
[(((((((triple9) -> rule9) triple9) -> rule6)) -> rule8))]
("rabbit" "is" "round" "-")
((((((triple9) -> (rule9 % int3)) triple9) -> (rule6 % int2))) -> (rule8 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int3
The rabbit sees the cat.
True
6
proof
[(((((((((triple9) -> rule9) triple9) -> rule6)) -> rule8)) -> rule9))]
("rabbit" "sees" "cat" "+")
((((((((triple9) -> (rule9 % int4)) triple9) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int3
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int4
The rabbit does not see the cat.
False
6
inv-proof
[(((((((((triple9) -> rule9) triple9) -> rule6)) -> rule8)) -> rule9))]
("rabbit" "sees" "cat" "-")
((((((((triple9) -> (rule9 % int4)) triple9) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int3
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int4
The rabbit is not red.
True
7
proof
[(((((((((((triple9) -> rule9) triple9) -> rule6)) -> rule8)) -> rule9)) -> rule1))]
("rabbit" "is" "red" "-")
((((((((((triple9) -> (rule9 % int5)) triple9) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
The rabbit is not red.
("rabbit" "is" "red" "-")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int4
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int5
The rabbit is red.
False
7
inv-proof
[(((((((((((triple9) -> rule9) triple9) -> rule6)) -> rule8)) -> rule9)) -> rule1))]
("rabbit" "is" "red" "+")
((((((((((triple9) -> (rule9 % int5)) triple9) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
The rabbit is not red.
("rabbit" "is" "red" "-")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int4
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int5
The lion does not see the cat.
Unknown
inv-rconc
[@1: The lion sees the cat.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("lion" "sees" "cat" "-")
The rabbit visits the cat.
Unknown
rconc
[@1: The rabbit visits the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "visits" "cat" "+")
The lion does not visit the cat.
Unknown
inv-rconc
[@1: The lion visits the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "visits" "cat" "-")
The cat sees the cat.
Unknown
rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("cat" "sees" "cat" "+")
The mouse does not need the cat.
Unknown
inv-random
[@0: The mouse needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "cat" "-")
The cat visits the rabbit.
Unknown
random
[@0: The cat visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "rabbit" "+")
The mouse is not nice.
Unknown
inv-random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
The lion does not visit the mouse.
Unknown
inv-random
[@0: The lion visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "mouse" "-")
The lion sees the mouse.
Unknown
random
[@0: The lion sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "mouse" "+")
The lion is not nice.
Unknown
inv-random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "-")
The cat sees the rabbit.
Unknown
random
[@0: The cat sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "rabbit" "+")
@0: The cat is not round.[(triple2)] The cat is red.[(triple1)] The cat needs the lion.[(triple3)] The cat sees the lion.[(triple4)] The cat visits the lion.[(triple5)] The lion is not round.[(triple6)] The lion needs the mouse.[(triple7)] The mouse is rough.[(triple8)] The mouse is round.[(triple9)] The mouse needs the lion.[(triple10)] The mouse needs the rabbit.[(triple11)] The mouse visits the cat.[(triple12 OR ((triple10) -> rule3))] The mouse visits the lion.[(triple13)] The mouse visits the rabbit.[(triple14)] The rabbit does not see the lion.[(triple15)] The rabbit visits the mouse.[(triple16)] @1: The cat visits the cat.[(((triple3) -> rule3))] The mouse sees the cat.[(((triple9) -> rule9))] @2: The cat needs the rabbit.[(((((triple9) -> rule9) triple9) -> rule6))] The mouse is not red.[(((((triple9) -> rule9)) -> rule1))] @3: The rabbit is round.[(((((((triple9) -> rule9) triple9) -> rule6)) -> rule8))] @4: The rabbit sees the cat.[(((((((((triple9) -> rule9) triple9) -> rule6)) -> rule8)) -> rule9))] @5: The rabbit is not red.[(((((((((((triple9) -> rule9) triple9) -> rule6)) -> rule8)) -> rule9)) -> rule1))]
The cat is not round.
("cat" "is" "round" "-")
triple2
The cat is red.
("cat" "is" "red" "+")
triple1
The cat needs the lion.
("cat" "needs" "lion" "+")
triple3
The cat sees the lion.
("cat" "sees" "lion" "+")
triple4
The cat visits the lion.
("cat" "visits" "lion" "+")
triple5
The lion is not round.
("lion" "is" "round" "-")
triple6
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple7
The mouse is rough.
("mouse" "is" "rough" "+")
triple8
The mouse is round.
("mouse" "is" "round" "+")
triple9
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple10
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple11
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple12
((triple10) -> (rule3 % int1))
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int1
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple13
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple14
The rabbit does not see the lion.
("rabbit" "sees" "lion" "-")
triple15
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple16
The cat visits the cat.
("cat" "visits" "cat" "+")
((triple3) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
((triple9) -> (rule9 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
((((triple9) -> (rule9 % int2)) triple9) -> (rule6 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The mouse is not red.
("mouse" "is" "red" "-")
((((triple9) -> (rule9 % int2))) -> (rule1 % int1))
The mouse is not red.
("mouse" "is" "red" "-")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
((((((triple9) -> (rule9 % int3)) triple9) -> (rule6 % int2))) -> (rule8 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int3
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
((((((((triple9) -> (rule9 % int4)) triple9) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int3
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int4
The rabbit is not red.
("rabbit" "is" "red" "-")
((((((((((triple9) -> (rule9 % int5)) triple9) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
The rabbit is not red.
("rabbit" "is" "red" "-")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int4
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int5