The dog needs the lion. The lion is young. Big things are young. If the lion needs the dog and the lion is not round then the dog eats the lion. If something is round then it eats the dog. If something is young and it needs the lion then the lion is kind. If something needs the lion and the lion likes the dog then it needs the dog. If something is big then it likes the dog. If something needs the lion then the lion is big. If something eats the dog and the dog does not eat the lion then it likes the lion.
The dog needs the lion.
("dog" "needs" "lion" "+")
The lion is young.
("lion" "is" "young" "+")
Big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If the lion needs the dog and the lion is not round then the dog eats the lion.
((("lion" "needs" "dog" "+") ("lion" "is" "round" "~")) -> ("dog" "eats" "lion" "+"))
If something is round then it eats the dog.
((("something" "is" "round" "+")) -> ("something" "eats" "dog" "+"))
If something is young and it needs the lion then the lion is kind.
((("something" "is" "young" "+") ("something" "needs" "lion" "+")) -> ("lion" "is" "kind" "+"))
If something needs the lion and the lion likes the dog then it needs the dog.
((("something" "needs" "lion" "+") ("lion" "likes" "dog" "+")) -> ("something" "needs" "dog" "+"))
If something is big then it likes the dog.
((("something" "is" "big" "+")) -> ("something" "likes" "dog" "+"))
If something needs the lion then the lion is big.
((("something" "needs" "lion" "+")) -> ("lion" "is" "big" "+"))
If something eats the dog and the dog does not eat the lion then it likes the lion.
((("something" "eats" "dog" "+") ("dog" "eats" "lion" "~")) -> ("something" "likes" "lion" "+"))
The dog needs the lion.
True
1
proof
[(triple1)]
("dog" "needs" "lion" "+")
triple1
The lion is not young.
False
1
inv-proof
[(triple2 OR ((((triple1) -> rule7)) -> rule1))]
("lion" "is" "young" "-")
triple2
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion is big.
True
2
proof
[(((triple1) -> rule7))]
("lion" "is" "big" "+")
((triple1) -> (rule7 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is not big.
False
2
inv-proof
[(((triple1) -> rule7))]
("lion" "is" "big" "-")
((triple1) -> (rule7 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion likes the dog.
True
3
proof
[(((((triple1) -> rule7)) -> rule6))]
("lion" "likes" "dog" "+")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The lion likes the dog.
("lion" "likes" "dog" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion does not like the dog.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule6))]
("lion" "likes" "dog" "-")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The lion likes the dog.
("lion" "likes" "dog" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The dog needs the dog.
True
5
proof
[(((triple1 ((((triple1) -> rule7)) -> rule6)) -> rule5))]
("dog" "needs" "dog" "+")
((triple1 ((((triple1) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The lion likes the dog.
("lion" "likes" "dog" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The dog does not need the dog.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule7)) -> rule6)) -> rule5))]
("dog" "needs" "dog" "-")
((triple1 ((((triple1) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The lion likes the dog.
("lion" "likes" "dog" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The lion is not kind.
Unknown
inv-rconc
[@2: The lion is kind.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("lion" "is" "kind" "-")
The dog eats the dog.
Unknown
rconc
[@1: The dog eats the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "eats" "dog" "+")
The dog is not young.
Unknown
inv-rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "young" "-")
The lion needs the dog.
Unknown
rconc
[@1: The lion needs the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "needs" "dog" "+")
The dog is not green.
Unknown
inv-random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The dog is round.
Unknown
random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "+")
@0: The dog needs the lion.[(triple1)] The lion is young.[(triple2 OR ((((triple1) -> rule7)) -> rule1))] @1: The lion is big.[(((triple1) -> rule7))] @2: The lion likes the dog.[(((((triple1) -> rule7)) -> rule6))] @3: The dog needs the dog.[(((triple1 ((((triple1) -> rule7)) -> rule6)) -> rule5))]
The dog needs the lion.
("dog" "needs" "lion" "+")
triple1
The lion is young.
("lion" "is" "young" "+")
triple2
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion is big.
("lion" "is" "big" "+")
((triple1) -> (rule7 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion likes the dog.
("lion" "likes" "dog" "+")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The lion likes the dog.
("lion" "likes" "dog" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
((triple1 ((((triple1) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The lion likes the dog.
("lion" "likes" "dog" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3