The cat is green. The cat is young. The cat needs the tiger. The rabbit visits the cat. The tiger is green. The tiger is young. The tiger likes the rabbit. The tiger needs the rabbit. The tiger visits the cat. The tiger visits the rabbit. If someone visits the cat then they like the rabbit. If someone likes the rabbit and they do not need the tiger then the rabbit likes the cat. If someone visits the tiger and the tiger is green then the tiger needs the cat. If someone needs the cat then they like the cat. If someone needs the rabbit then they do not like the tiger. If someone is green then they visit the tiger. If the cat visits the tiger and the cat does not need the tiger then the cat visits the rabbit. If someone likes the rabbit then the rabbit visits the tiger.
The cat is green.
("cat" "is" "green" "+")
The cat is young.
("cat" "is" "young" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If someone visits the cat then they like the rabbit.
((("someone" "visits" "cat" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone likes the rabbit and they do not need the tiger then the rabbit likes the cat.
((("someone" "likes" "rabbit" "+") ("someone" "needs" "tiger" "~")) -> ("rabbit" "likes" "cat" "+"))
If someone visits the tiger and the tiger is green then the tiger needs the cat.
((("someone" "visits" "tiger" "+") ("tiger" "is" "green" "+")) -> ("tiger" "needs" "cat" "+"))
If someone needs the cat then they like the cat.
((("someone" "needs" "cat" "+")) -> ("someone" "likes" "cat" "+"))
If someone needs the rabbit then they do not like the tiger.
((("someone" "needs" "rabbit" "+")) -> ("someone" "likes" "tiger" "-"))
If someone is green then they visit the tiger.
((("someone" "is" "green" "+")) -> ("someone" "visits" "tiger" "+"))
If the cat visits the tiger and the cat does not need the tiger then the cat visits the rabbit.
((("cat" "visits" "tiger" "+") ("cat" "needs" "tiger" "~")) -> ("cat" "visits" "rabbit" "+"))
If someone likes the rabbit then the rabbit visits the tiger.
((("someone" "likes" "rabbit" "+")) -> ("rabbit" "visits" "tiger" "+"))
The tiger is green.
True
1
proof
[(triple5)]
("tiger" "is" "green" "+")
triple5
The tiger is not green.
False
1
inv-proof
[(triple5)]
("tiger" "is" "green" "-")
triple5
The tiger does not like the tiger.
True
2
proof
[(((triple8) -> rule5))]
("tiger" "likes" "tiger" "-")
((triple8) -> (rule5 % int1))
The tiger does not like the tiger.
("tiger" "likes" "tiger" "-")
int1
The rabbit does not like the rabbit.
False
2
inv-proof
[(((triple4) -> rule1))]
("rabbit" "likes" "rabbit" "-")
((triple4) -> (rule1 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The tiger needs the cat.
True
4
proof
[(((((triple1) -> rule6) triple5) -> rule3) OR ((((triple5) -> rule6) triple5) -> rule3) OR ((((triple7) -> rule8) triple5) -> rule3) OR ((((((triple4) -> rule1)) -> rule8) triple5) -> rule3) OR ((((((triple9) -> rule1)) -> rule8) triple5) -> rule3))]
("tiger" "needs" "cat" "+")
((((triple1) -> (rule6 % int2)) triple5) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int2
((((triple5) -> (rule6 % int2)) triple5) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
((((triple7) -> (rule8 % int2)) triple5) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
((((((triple4) -> (rule1 % int3))) -> (rule8 % int2)) triple5) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int3
((((((triple9) -> (rule1 % int3))) -> (rule8 % int2)) triple5) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int3
The tiger does not need the cat.
False
4
inv-proof
[(((((triple1) -> rule6) triple5) -> rule3) OR ((((triple5) -> rule6) triple5) -> rule3) OR ((((triple7) -> rule8) triple5) -> rule3) OR ((((((triple4) -> rule1)) -> rule8) triple5) -> rule3) OR ((((((triple9) -> rule1)) -> rule8) triple5) -> rule3))]
("tiger" "needs" "cat" "-")
((((triple1) -> (rule6 % int2)) triple5) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int2
((((triple5) -> (rule6 % int2)) triple5) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
((((triple7) -> (rule8 % int2)) triple5) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
((((((triple4) -> (rule1 % int3))) -> (rule8 % int2)) triple5) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int3
((((((triple9) -> (rule1 % int3))) -> (rule8 % int2)) triple5) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int3
The tiger likes the cat.
True
5
proof
[(((((((triple1) -> rule6) triple5) -> rule3)) -> rule4) OR ((((((triple5) -> rule6) triple5) -> rule3)) -> rule4) OR ((((((triple7) -> rule8) triple5) -> rule3)) -> rule4) OR ((((((((triple4) -> rule1)) -> rule8) triple5) -> rule3)) -> rule4) OR ((((((((triple9) -> rule1)) -> rule8) triple5) -> rule3)) -> rule4))]
("tiger" "likes" "cat" "+")
((((((triple1) -> (rule6 % int3)) triple5) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int3
((((((triple5) -> (rule6 % int3)) triple5) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int3
((((((triple7) -> (rule8 % int3)) triple5) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int3
((((((((triple4) -> (rule1 % int4))) -> (rule8 % int3)) triple5) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int3
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int4
((((((((triple9) -> (rule1 % int4))) -> (rule8 % int3)) triple5) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int3
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int4
The tiger does not like the cat.
False
5
inv-proof
[(((((((triple1) -> rule6) triple5) -> rule3)) -> rule4) OR ((((((triple5) -> rule6) triple5) -> rule3)) -> rule4) OR ((((((triple7) -> rule8) triple5) -> rule3)) -> rule4) OR ((((((((triple4) -> rule1)) -> rule8) triple5) -> rule3)) -> rule4) OR ((((((((triple9) -> rule1)) -> rule8) triple5) -> rule3)) -> rule4))]
("tiger" "likes" "cat" "-")
((((((triple1) -> (rule6 % int3)) triple5) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int3
((((((triple5) -> (rule6 % int3)) triple5) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int3
((((((triple7) -> (rule8 % int3)) triple5) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int3
((((((((triple4) -> (rule1 % int4))) -> (rule8 % int3)) triple5) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int3
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int4
((((((((triple9) -> (rule1 % int4))) -> (rule8 % int3)) triple5) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int3
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int4
The cat does not like the cat.
Unknown
inv-rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "likes" "cat" "-")
The rabbit likes the cat.
Unknown
rconc
[@1: The rabbit likes the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "likes" "cat" "+")
The cat does not visit the rabbit.
Unknown
inv-rconc
[@1: The cat visits the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "visits" "rabbit" "-")
The cat likes the rabbit.
Unknown
rconc
[@1: The cat likes the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "rabbit" "+")
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
The rabbit needs the cat.
Unknown
random
[@0: The rabbit needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "cat" "+")
The rabbit is not young.
Unknown
inv-random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "-")
The rabbit needs the tiger.
Unknown
random
[@0: The rabbit needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "tiger" "+")
@0: The cat is green.[(triple1)] The cat is young.[(triple2)] The cat needs the tiger.[(triple3)] The rabbit visits the cat.[(triple4)] The tiger is green.[(triple5)] The tiger is young.[(triple6)] The tiger likes the rabbit.[(triple7 OR ((triple9) -> rule1))] The tiger needs the rabbit.[(triple8)] The tiger visits the cat.[(triple9)] The tiger visits the rabbit.[(triple10)] @1: The cat visits the tiger.[(((triple1) -> rule6))] The rabbit likes the rabbit.[(((triple4) -> rule1))] The rabbit visits the tiger.[(((triple7) -> rule8) OR ((((triple4) -> rule1)) -> rule8) OR ((((triple9) -> rule1)) -> rule8))] The tiger does not like the tiger.[(((triple8) -> rule5))] The tiger visits the tiger.[(((triple5) -> rule6))] @2: The tiger needs the cat.[(((((triple1) -> rule6) triple5) -> rule3) OR ((((triple5) -> rule6) triple5) -> rule3) OR ((((triple7) -> rule8) triple5) -> rule3) OR ((((((triple4) -> rule1)) -> rule8) triple5) -> rule3) OR ((((((triple9) -> rule1)) -> rule8) triple5) -> rule3))] @3: The tiger likes the cat.[(((((((triple1) -> rule6) triple5) -> rule3)) -> rule4) OR ((((((triple5) -> rule6) triple5) -> rule3)) -> rule4) OR ((((((triple7) -> rule8) triple5) -> rule3)) -> rule4) OR ((((((((triple4) -> rule1)) -> rule8) triple5) -> rule3)) -> rule4) OR ((((((((triple9) -> rule1)) -> rule8) triple5) -> rule3)) -> rule4))]
The cat is green.
("cat" "is" "green" "+")
triple1
The cat is young.
("cat" "is" "young" "+")
triple2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple3
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple4
The tiger is green.
("tiger" "is" "green" "+")
triple5
The tiger is young.
("tiger" "is" "young" "+")
triple6
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple7
((triple9) -> (rule1 % int1))
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int1
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple8
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple9
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple10
The cat visits the tiger.
("cat" "visits" "tiger" "+")
((triple1) -> (rule6 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((triple4) -> (rule1 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
((triple7) -> (rule8 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule8 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
((((triple9) -> (rule1 % int2))) -> (rule8 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int2
The tiger does not like the tiger.
("tiger" "likes" "tiger" "-")
((triple8) -> (rule5 % int1))
The tiger does not like the tiger.
("tiger" "likes" "tiger" "-")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple5) -> (rule6 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
((((triple1) -> (rule6 % int2)) triple5) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int2
((((triple5) -> (rule6 % int2)) triple5) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
((((triple7) -> (rule8 % int2)) triple5) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
((((((triple4) -> (rule1 % int3))) -> (rule8 % int2)) triple5) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int3
((((((triple9) -> (rule1 % int3))) -> (rule8 % int2)) triple5) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int3
The tiger likes the cat.
("tiger" "likes" "cat" "+")
((((((triple1) -> (rule6 % int3)) triple5) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int3
((((((triple5) -> (rule6 % int3)) triple5) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int3
((((((triple7) -> (rule8 % int3)) triple5) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int3
((((((((triple4) -> (rule1 % int4))) -> (rule8 % int3)) triple5) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int3
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int4
((((((((triple9) -> (rule1 % int4))) -> (rule8 % int3)) triple5) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int3
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int4