The cat eats the lion. The cat is not nice. The cat sees the cow. The cow sees the lion. The dog sees the lion. The lion is not cold. The lion needs the dog. If something is green then it is not young. If the cow sees the lion then the lion is green. If something eats the cat then the cat needs the cow.
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat is not nice.
("cat" "is" "nice" "-")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion is not cold.
("lion" "is" "cold" "-")
The lion needs the dog.
("lion" "needs" "dog" "+")
If something is green then it is not young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "-"))
If the cow sees the lion then the lion is green.
((("cow" "sees" "lion" "+")) -> ("lion" "is" "green" "+"))
If something eats the cat then the cat needs the cow.
((("something" "eats" "cat" "+")) -> ("cat" "needs" "cow" "+"))
The dog sees the lion.
True
1
proof
[(triple5)]
("dog" "sees" "lion" "+")
triple5
The lion does not need the dog.
False
1
inv-proof
[(triple7)]
("lion" "needs" "dog" "-")
triple7
The lion is green.
True
2
proof
[(((triple4) -> rule2))]
("lion" "is" "green" "+")
((triple4) -> (rule2 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is not green.
False
2
inv-proof
[(((triple4) -> rule2))]
("lion" "is" "green" "-")
((triple4) -> (rule2 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is not young.
True
3
proof
[(((((triple4) -> rule2)) -> rule1))]
("lion" "is" "young" "-")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The lion is not young.
("lion" "is" "young" "-")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion is young.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule1))]
("lion" "is" "young" "+")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The lion is not young.
("lion" "is" "young" "-")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The cat does not need the cow.
Unknown
inv-rconc
[@1: The cat needs the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "needs" "cow" "-")
The cow needs the cat.
Unknown
random
[@0: The cow needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cat" "+")
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
The dog is not nice.
Unknown
inv-random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "-")
The cat eats the cow.
Unknown
random
[@0: The cat eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cow" "+")
@0: The cat eats the lion.[(triple1)] The cat is not nice.[(triple2)] The cat sees the cow.[(triple3)] The cow sees the lion.[(triple4)] The dog sees the lion.[(triple5)] The lion is not cold.[(triple6)] The lion needs the dog.[(triple7)] @1: The lion is green.[(((triple4) -> rule2))] @2: The lion is not young.[(((((triple4) -> rule2)) -> rule1))]
The cat eats the lion.
("cat" "eats" "lion" "+")
triple1
The cat is not nice.
("cat" "is" "nice" "-")
triple2
The cat sees the cow.
("cat" "sees" "cow" "+")
triple3
The cow sees the lion.
("cow" "sees" "lion" "+")
triple4
The dog sees the lion.
("dog" "sees" "lion" "+")
triple5
The lion is not cold.
("lion" "is" "cold" "-")
triple6
The lion needs the dog.
("lion" "needs" "dog" "+")
triple7
The lion is green.
("lion" "is" "green" "+")
((triple4) -> (rule2 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is not young.
("lion" "is" "young" "-")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The lion is not young.
("lion" "is" "young" "-")
int1
The lion is green.
("lion" "is" "green" "+")
int2