The cat needs the lion. The cow is nice. The cow visits the tiger. The lion is cold. The tiger likes the cat. The tiger needs the cow. The tiger visits the cow. If something likes the tiger then the tiger is blue. If something needs the cow then it is nice. If something likes the lion and it needs the cat then the lion likes the cow. If something likes the lion then it is round. If something likes the tiger then the tiger likes the lion. If something is nice then it likes the tiger. If something visits the tiger and the tiger visits the lion then it likes the tiger. If something is blue then it likes the cow.
The cat needs the lion.
("cat" "needs" "lion" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The lion is cold.
("lion" "is" "cold" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If something likes the tiger then the tiger is blue.
((("something" "likes" "tiger" "+")) -> ("tiger" "is" "blue" "+"))
If something needs the cow then it is nice.
((("something" "needs" "cow" "+")) -> ("something" "is" "nice" "+"))
If something likes the lion and it needs the cat then the lion likes the cow.
((("something" "likes" "lion" "+") ("something" "needs" "cat" "+")) -> ("lion" "likes" "cow" "+"))
If something likes the lion then it is round.
((("something" "likes" "lion" "+")) -> ("something" "is" "round" "+"))
If something likes the tiger then the tiger likes the lion.
((("something" "likes" "tiger" "+")) -> ("tiger" "likes" "lion" "+"))
If something is nice then it likes the tiger.
((("something" "is" "nice" "+")) -> ("something" "likes" "tiger" "+"))
If something visits the tiger and the tiger visits the lion then it likes the tiger.
((("something" "visits" "tiger" "+") ("tiger" "visits" "lion" "+")) -> ("something" "likes" "tiger" "+"))
If something is blue then it likes the cow.
((("something" "is" "blue" "+")) -> ("something" "likes" "cow" "+"))
The lion is cold.
True
1
proof
[(triple4)]
("lion" "is" "cold" "+")
triple4
The cow is not nice.
False
1
inv-proof
[(triple2)]
("cow" "is" "nice" "-")
triple2
The tiger is nice.
True
2
proof
[(((triple6) -> rule2))]
("tiger" "is" "nice" "+")
((triple6) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is not nice.
False
2
inv-proof
[(((triple6) -> rule2))]
("tiger" "is" "nice" "-")
((triple6) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger likes the tiger.
True
3
proof
[(((((triple6) -> rule2)) -> rule6))]
("tiger" "likes" "tiger" "+")
((((triple6) -> (rule2 % int2))) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger does not like the tiger.
False
3
inv-proof
[(((((triple6) -> rule2)) -> rule6))]
("tiger" "likes" "tiger" "-")
((((triple6) -> (rule2 % int2))) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is round.
True
4
proof
[(((((((triple2) -> rule6)) -> rule5)) -> rule4) OR ((((((((triple6) -> rule2)) -> rule6)) -> rule5)) -> rule4))]
("tiger" "is" "round" "+")
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int3
((((((((triple6) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger is nice.
("tiger" "is" "nice" "+")
int4
The tiger is not round.
False
4
inv-proof
[(((((((triple2) -> rule6)) -> rule5)) -> rule4) OR ((((((((triple6) -> rule2)) -> rule6)) -> rule5)) -> rule4))]
("tiger" "is" "round" "-")
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int3
((((((((triple6) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger is nice.
("tiger" "is" "nice" "+")
int4
The lion does not like the cow.
Unknown
inv-rconc
[@1: The lion likes the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "likes" "cow" "-")
The lion is round.
Unknown
rconc
[@1: The lion is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "round" "+")
The lion is not nice.
Unknown
inv-rconc
[@1: The lion is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "nice" "-")
The cat likes the tiger.
Unknown
rconc
[@2: The cat likes the tiger.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("cat" "likes" "tiger" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The cow needs the cat.
Unknown
random
[@0: The cow needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cat" "+")
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
@0: The cat needs the lion.[(triple1)] The cow is nice.[(triple2)] The cow visits the tiger.[(triple3)] The lion is cold.[(triple4)] The tiger likes the cat.[(triple5)] The tiger needs the cow.[(triple6)] The tiger visits the cow.[(triple7)] @1: The cow likes the tiger.[(((triple2) -> rule6))] The tiger is nice.[(((triple6) -> rule2))] @2: The tiger is blue.[(((((triple2) -> rule6)) -> rule1) OR ((((((triple6) -> rule2)) -> rule6)) -> rule1))] The tiger likes the lion.[(((((triple2) -> rule6)) -> rule5) OR ((((((triple6) -> rule2)) -> rule6)) -> rule5))] The tiger likes the tiger.[(((((triple6) -> rule2)) -> rule6))] @3: The tiger is round.[(((((((triple2) -> rule6)) -> rule5)) -> rule4) OR ((((((((triple6) -> rule2)) -> rule6)) -> rule5)) -> rule4))] The tiger likes the cow.[(((((((triple2) -> rule6)) -> rule1)) -> rule8) OR ((((((((triple6) -> rule2)) -> rule6)) -> rule1)) -> rule8))]
The cat needs the lion.
("cat" "needs" "lion" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
triple2
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple3
The lion is cold.
("lion" "is" "cold" "+")
triple4
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple5
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple6
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple7
The cow likes the tiger.
("cow" "likes" "tiger" "+")
((triple2) -> (rule6 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
((triple6) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int2
((((((triple6) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The tiger likes the lion.
("tiger" "likes" "lion" "+")
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int2
((((((triple6) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((((triple6) -> (rule2 % int2))) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int3
((((((((triple6) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger is nice.
("tiger" "is" "nice" "+")
int4
The tiger likes the cow.
("tiger" "likes" "cow" "+")
((((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int3
((((((((triple6) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger is nice.
("tiger" "is" "nice" "+")
int4