The cat is kind. The cat needs the tiger. The cat visits the lion. The cow is red. The cow is young. The cow needs the lion. The cow visits the cat. The lion is young. The lion likes the cow. The lion needs the tiger. The tiger is red. The tiger likes the cow. The tiger likes the lion. The tiger needs the cow. The tiger needs the lion. The tiger visits the cat. If something likes the cat then the cat is kind. If the cow is young and the cow visits the tiger then the tiger is young. Young things are kind. If the tiger visits the lion then the lion is young. If something likes the lion then it visits the cat. If the cow needs the lion then the cow visits the tiger.
The cat is kind.
("cat" "is" "kind" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is young.
("cow" "is" "young" "+")
The cow needs the lion.
("cow" "needs" "lion" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes the cow.
("lion" "likes" "cow" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If something likes the cat then the cat is kind.
((("something" "likes" "cat" "+")) -> ("cat" "is" "kind" "+"))
If the cow is young and the cow visits the tiger then the tiger is young.
((("cow" "is" "young" "+") ("cow" "visits" "tiger" "+")) -> ("tiger" "is" "young" "+"))
Young things are kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
If the tiger visits the lion then the lion is young.
((("tiger" "visits" "lion" "+")) -> ("lion" "is" "young" "+"))
If something likes the lion then it visits the cat.
((("something" "likes" "lion" "+")) -> ("something" "visits" "cat" "+"))
If the cow needs the lion then the cow visits the tiger.
((("cow" "needs" "lion" "+")) -> ("cow" "visits" "tiger" "+"))
The tiger needs the lion.
True
1
proof
[(triple15)]
("tiger" "needs" "lion" "+")
triple15
The cow is not young.
False
1
inv-proof
[(triple5)]
("cow" "is" "young" "-")
triple5
The cow visits the tiger.
True
2
proof
[(((triple6) -> rule6))]
("cow" "visits" "tiger" "+")
((triple6) -> (rule6 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The cow is not kind.
False
2
inv-proof
[(((triple5) -> rule3))]
("cow" "is" "kind" "-")
((triple5) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The tiger is young.
True
4
proof
[(((triple5 ((triple6) -> rule6)) -> rule2))]
("tiger" "is" "young" "+")
((triple5 ((triple6) -> (rule6 % int2))) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int2
The tiger is not young.
False
4
inv-proof
[(((triple5 ((triple6) -> rule6)) -> rule2))]
("tiger" "is" "young" "-")
((triple5 ((triple6) -> (rule6 % int2))) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int2
The tiger is kind.
True
5
proof
[(((((triple5 ((triple6) -> rule6)) -> rule2)) -> rule3))]
("tiger" "is" "kind" "+")
((((triple5 ((triple6) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int3
The tiger is not kind.
False
5
inv-proof
[(((((triple5 ((triple6) -> rule6)) -> rule2)) -> rule3))]
("tiger" "is" "kind" "-")
((((triple5 ((triple6) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int3
The lion does not visit the cat.
Unknown
inv-rconc
[@1: The lion visits the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "visits" "cat" "-")
The cat visits the cat.
Unknown
rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "visits" "cat" "+")
The cow is not round.
Unknown
inv-random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
The lion does not like the cat.
Unknown
inv-random
[@0: The lion likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "cat" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
The cat does not like the cow.
Unknown
inv-random
[@0: The cat likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cow" "-")
The cat is red.
Unknown
random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "+")
@0: The cat is kind.[(triple1)] The cat needs the tiger.[(triple2)] The cat visits the lion.[(triple3)] The cow is red.[(triple4)] The cow is young.[(triple5)] The cow needs the lion.[(triple6)] The cow visits the cat.[(triple7)] The lion is young.[(triple8)] The lion likes the cow.[(triple9)] The lion needs the tiger.[(triple10)] The tiger is red.[(triple11)] The tiger likes the cow.[(triple12)] The tiger likes the lion.[(triple13)] The tiger needs the cow.[(triple14)] The tiger needs the lion.[(triple15)] The tiger visits the cat.[(triple16 OR ((triple13) -> rule5))] @1: The cow is kind.[(((triple5) -> rule3))] The cow visits the tiger.[(((triple6) -> rule6))] The lion is kind.[(((triple8) -> rule3))] @2: The tiger is young.[(((triple5 ((triple6) -> rule6)) -> rule2))] @3: The tiger is kind.[(((((triple5 ((triple6) -> rule6)) -> rule2)) -> rule3))]
The cat is kind.
("cat" "is" "kind" "+")
triple1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple2
The cat visits the lion.
("cat" "visits" "lion" "+")
triple3
The cow is red.
("cow" "is" "red" "+")
triple4
The cow is young.
("cow" "is" "young" "+")
triple5
The cow needs the lion.
("cow" "needs" "lion" "+")
triple6
The cow visits the cat.
("cow" "visits" "cat" "+")
triple7
The lion is young.
("lion" "is" "young" "+")
triple8
The lion likes the cow.
("lion" "likes" "cow" "+")
triple9
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple10
The tiger is red.
("tiger" "is" "red" "+")
triple11
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple12
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple13
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple14
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple15
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple16
((triple13) -> (rule5 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
((triple5) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow visits the tiger.
("cow" "visits" "tiger" "+")
((triple6) -> (rule6 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
((triple8) -> (rule3 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
((triple5 ((triple6) -> (rule6 % int2))) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
((((triple5 ((triple6) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int3