The cat is blue. The cat is rough. The cat needs the lion. The lion eats the rabbit. The lion is not blue. The lion is green. The lion needs the cat. The lion needs the rabbit. The lion visits the cat. The rabbit is blue. The rabbit is rough. The rabbit is young. The rabbit needs the cat. The rabbit does not need the lion. The rabbit visits the cat. If something is green and it eats the cat then it needs the rabbit. If something eats the cat and it does not eat the rabbit then it does not eat the lion. If something needs the lion and it visits the rabbit then the lion is rough. If something eats the lion then it visits the rabbit. If something visits the cat then the cat eats the lion. If something needs the rabbit and it does not visit the cat then the cat needs the lion. If the lion needs the rabbit then the rabbit does not eat the cat. If something is young and it needs the lion then the lion visits the rabbit.
The cat is blue.
("cat" "is" "blue" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion is not blue.
("lion" "is" "blue" "-")
The lion is green.
("lion" "is" "green" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The rabbit does not need the lion.
("rabbit" "needs" "lion" "-")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
If something is green and it eats the cat then it needs the rabbit.
((("something" "is" "green" "+") ("something" "eats" "cat" "+")) -> ("something" "needs" "rabbit" "+"))
If something eats the cat and it does not eat the rabbit then it does not eat the lion.
((("something" "eats" "cat" "+") ("something" "eats" "rabbit" "~")) -> ("something" "eats" "lion" "-"))
If something needs the lion and it visits the rabbit then the lion is rough.
((("something" "needs" "lion" "+") ("something" "visits" "rabbit" "+")) -> ("lion" "is" "rough" "+"))
If something eats the lion then it visits the rabbit.
((("something" "eats" "lion" "+")) -> ("something" "visits" "rabbit" "+"))
If something visits the cat then the cat eats the lion.
((("something" "visits" "cat" "+")) -> ("cat" "eats" "lion" "+"))
If something needs the rabbit and it does not visit the cat then the cat needs the lion.
((("something" "needs" "rabbit" "+") ("something" "visits" "cat" "~")) -> ("cat" "needs" "lion" "+"))
If the lion needs the rabbit then the rabbit does not eat the cat.
((("lion" "needs" "rabbit" "+")) -> ("rabbit" "eats" "cat" "-"))
If something is young and it needs the lion then the lion visits the rabbit.
((("something" "is" "young" "+") ("something" "needs" "lion" "+")) -> ("lion" "visits" "rabbit" "+"))
The lion needs the cat.
True
1
proof
[(triple7)]
("lion" "needs" "cat" "+")
triple7
The lion does not visit the cat.
False
1
inv-proof
[(triple9)]
("lion" "visits" "cat" "-")
triple9
The rabbit does not eat the cat.
True
2
proof
[(((triple8) -> rule7))]
("rabbit" "eats" "cat" "-")
((triple8) -> (rule7 % int1))
The rabbit does not eat the cat.
("rabbit" "eats" "cat" "-")
int1
The rabbit eats the cat.
False
2
inv-proof
[(((triple8) -> rule7))]
("rabbit" "eats" "cat" "+")
((triple8) -> (rule7 % int1))
The rabbit does not eat the cat.
("rabbit" "eats" "cat" "-")
int1
The cat visits the rabbit.
True
3
proof
[(((((triple15) -> rule5)) -> rule4) OR ((((triple9) -> rule5)) -> rule4))]
("cat" "visits" "rabbit" "+")
((((triple15) -> (rule5 % int2))) -> (rule4 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
int2
((((triple9) -> (rule5 % int2))) -> (rule4 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
int2
The cat does not visit the rabbit.
False
3
inv-proof
[(((((triple15) -> rule5)) -> rule4) OR ((((triple9) -> rule5)) -> rule4))]
("cat" "visits" "rabbit" "-")
((((triple15) -> (rule5 % int2))) -> (rule4 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
int2
((((triple9) -> (rule5 % int2))) -> (rule4 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
int2
The lion is rough.
True
5
proof
[(((triple3 ((((triple15) -> rule5)) -> rule4)) -> rule3) OR ((triple3 ((((triple9) -> rule5)) -> rule4)) -> rule3))]
("lion" "is" "rough" "+")
((triple3 ((((triple15) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The cat eats the lion.
("cat" "eats" "lion" "+")
int3
((triple3 ((((triple9) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The cat eats the lion.
("cat" "eats" "lion" "+")
int3
The lion is not rough.
False
5
inv-proof
[(((triple3 ((((triple15) -> rule5)) -> rule4)) -> rule3) OR ((triple3 ((((triple9) -> rule5)) -> rule4)) -> rule3))]
("lion" "is" "rough" "-")
((triple3 ((((triple15) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The cat eats the lion.
("cat" "eats" "lion" "+")
int3
((triple3 ((((triple9) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The cat eats the lion.
("cat" "eats" "lion" "+")
int3
The cat does not need the rabbit.
Unknown
inv-rconc
[@1: The cat needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "needs" "rabbit" "-")
The rabbit needs the rabbit.
Unknown
rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "needs" "rabbit" "+")
The lion does not visit the rabbit.
Unknown
inv-rconc
[@1: The lion visits the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "visits" "rabbit" "-")
The rabbit visits the rabbit.
Unknown
rconc
[@1: The rabbit visits the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "visits" "rabbit" "+")
The cat is not young.
Unknown
inv-random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
The cat does not visit the lion.
Unknown
inv-random
[@0: The cat visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "lion" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat is blue.[(triple1)] The cat is rough.[(triple2)] The cat needs the lion.[(triple3)] The lion eats the rabbit.[(triple4)] The lion is green.[(triple6)] The lion is not blue.[(triple5)] The lion needs the cat.[(triple7)] The lion needs the rabbit.[(triple8)] The lion visits the cat.[(triple9)] The rabbit does not need the lion.[(triple14)] The rabbit is blue.[(triple10)] The rabbit is rough.[(triple11)] The rabbit is young.[(triple12)] The rabbit needs the cat.[(triple13)] The rabbit visits the cat.[(triple15)] @1: The cat eats the lion.[(((triple15) -> rule5) OR ((triple9) -> rule5))] The rabbit does not eat the cat.[(((triple8) -> rule7))] @2: The cat visits the rabbit.[(((((triple15) -> rule5)) -> rule4) OR ((((triple9) -> rule5)) -> rule4))] @3: The lion is rough.[(((triple3 ((((triple15) -> rule5)) -> rule4)) -> rule3) OR ((triple3 ((((triple9) -> rule5)) -> rule4)) -> rule3))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
The cat needs the lion.
("cat" "needs" "lion" "+")
triple3
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple4
The lion is green.
("lion" "is" "green" "+")
triple6
The lion is not blue.
("lion" "is" "blue" "-")
triple5
The lion needs the cat.
("lion" "needs" "cat" "+")
triple7
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple8
The lion visits the cat.
("lion" "visits" "cat" "+")
triple9
The rabbit does not need the lion.
("rabbit" "needs" "lion" "-")
triple14
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple10
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple11
The rabbit is young.
("rabbit" "is" "young" "+")
triple12
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple13
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple15
The cat eats the lion.
("cat" "eats" "lion" "+")
((triple15) -> (rule5 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
((triple9) -> (rule5 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
The rabbit does not eat the cat.
("rabbit" "eats" "cat" "-")
((triple8) -> (rule7 % int1))
The rabbit does not eat the cat.
("rabbit" "eats" "cat" "-")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
((((triple15) -> (rule5 % int2))) -> (rule4 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
int2
((((triple9) -> (rule5 % int2))) -> (rule4 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
((triple3 ((((triple15) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The cat eats the lion.
("cat" "eats" "lion" "+")
int3
((triple3 ((((triple9) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The cat eats the lion.
("cat" "eats" "lion" "+")
int3