The dog eats the lion. The lion eats the dog. If something eats the lion then it is blue. If something needs the dog and it chases the lion then the dog is not nice. If something needs the dog and it is blue then it does not chase the dog. If something needs the dog and it does not chase the lion then it eats the lion. If something is cold then it does not eat the lion. If something is blue then it needs the dog. If something eats the dog then the dog is blue. If the lion does not need the dog then the lion is nice.
The dog eats the lion.
("dog" "eats" "lion" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
If something eats the lion then it is blue.
((("something" "eats" "lion" "+")) -> ("something" "is" "blue" "+"))
If something needs the dog and it chases the lion then the dog is not nice.
((("something" "needs" "dog" "+") ("something" "chases" "lion" "+")) -> ("dog" "is" "nice" "-"))
If something needs the dog and it is blue then it does not chase the dog.
((("something" "needs" "dog" "+") ("something" "is" "blue" "+")) -> ("something" "chases" "dog" "-"))
If something needs the dog and it does not chase the lion then it eats the lion.
((("something" "needs" "dog" "+") ("something" "chases" "lion" "~")) -> ("something" "eats" "lion" "+"))
If something is cold then it does not eat the lion.
((("something" "is" "cold" "+")) -> ("something" "eats" "lion" "-"))
If something is blue then it needs the dog.
((("something" "is" "blue" "+")) -> ("something" "needs" "dog" "+"))
If something eats the dog then the dog is blue.
((("something" "eats" "dog" "+")) -> ("dog" "is" "blue" "+"))
If the lion does not need the dog then the lion is nice.
((("lion" "needs" "dog" "~")) -> ("lion" "is" "nice" "+"))
The lion eats the dog.
True
1
proof
[(triple2)]
("lion" "eats" "dog" "+")
triple2
The dog does not eat the lion.
False
1
inv-proof
[(triple1)]
("dog" "eats" "lion" "-")
triple1
The dog is blue.
True
2
proof
[(((triple1) -> rule1) OR ((triple2) -> rule7))]
("dog" "is" "blue" "+")
((triple1) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
((triple2) -> (rule7 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is not blue.
False
2
inv-proof
[(((triple1) -> rule1) OR ((triple2) -> rule7))]
("dog" "is" "blue" "-")
((triple1) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
((triple2) -> (rule7 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog needs the dog.
True
3
proof
[(((((triple1) -> rule1)) -> rule6) OR ((((triple2) -> rule7)) -> rule6))]
("dog" "needs" "dog" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog does not need the dog.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule6) OR ((((triple2) -> rule7)) -> rule6))]
("dog" "needs" "dog" "-")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog does not chase the dog.
True
6
proof
[(((((((triple1) -> rule1)) -> rule6) ((triple1) -> rule1)) -> rule3) OR ((((((triple1) -> rule1)) -> rule6) ((triple2) -> rule7)) -> rule3) OR ((((((triple2) -> rule7)) -> rule6) ((triple1) -> rule1)) -> rule3) OR ((((((triple2) -> rule7)) -> rule6) ((triple2) -> rule7)) -> rule3))]
("dog" "chases" "dog" "-")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2)) ((triple1) -> (rule1 % int3))) -> (rule3 % int1))
The dog does not chase the dog.
("dog" "chases" "dog" "-")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2)) ((triple2) -> (rule7 % int3))) -> (rule3 % int1))
The dog does not chase the dog.
("dog" "chases" "dog" "-")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
((((((triple2) -> (rule7 % int3))) -> (rule6 % int2)) ((triple1) -> (rule1 % int3))) -> (rule3 % int1))
The dog does not chase the dog.
("dog" "chases" "dog" "-")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
((((((triple2) -> (rule7 % int3))) -> (rule6 % int2)) ((triple2) -> (rule7 % int3))) -> (rule3 % int1))
The dog does not chase the dog.
("dog" "chases" "dog" "-")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
The dog chases the dog.
False
6
inv-proof
[(((((((triple1) -> rule1)) -> rule6) ((triple1) -> rule1)) -> rule3) OR ((((((triple1) -> rule1)) -> rule6) ((triple2) -> rule7)) -> rule3) OR ((((((triple2) -> rule7)) -> rule6) ((triple1) -> rule1)) -> rule3) OR ((((((triple2) -> rule7)) -> rule6) ((triple2) -> rule7)) -> rule3))]
("dog" "chases" "dog" "+")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2)) ((triple1) -> (rule1 % int3))) -> (rule3 % int1))
The dog does not chase the dog.
("dog" "chases" "dog" "-")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2)) ((triple2) -> (rule7 % int3))) -> (rule3 % int1))
The dog does not chase the dog.
("dog" "chases" "dog" "-")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
((((((triple2) -> (rule7 % int3))) -> (rule6 % int2)) ((triple1) -> (rule1 % int3))) -> (rule3 % int1))
The dog does not chase the dog.
("dog" "chases" "dog" "-")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
((((((triple2) -> (rule7 % int3))) -> (rule6 % int2)) ((triple2) -> (rule7 % int3))) -> (rule3 % int1))
The dog does not chase the dog.
("dog" "chases" "dog" "-")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
The lion does not eat the lion.
Unknown
inv-rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "eats" "lion" "-")
The lion needs the dog.
Unknown
rconc
[@3: The lion needs the dog.[CWA. Example of deepest failure = (rule6 <- rule1 <- rule4 <- FAIL)]]
("lion" "needs" "dog" "+")
The lion is not blue.
Unknown
inv-rconc
[@2: The lion is blue.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("lion" "is" "blue" "-")
The lion is nice.
Unknown
rconc
[@1: The lion is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "is" "nice" "+")
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
The lion is not cold.
Unknown
inv-random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "-")
The dog is green.
Unknown
random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "+")
@0: The dog eats the lion.[(triple1)] The lion eats the dog.[(triple2)] @1: The dog is blue.[(((triple1) -> rule1) OR ((triple2) -> rule7))] @2: The dog needs the dog.[(((((triple1) -> rule1)) -> rule6) OR ((((triple2) -> rule7)) -> rule6))] @3: The dog does not chase the dog.[(((((((triple1) -> rule1)) -> rule6) ((triple1) -> rule1)) -> rule3) OR ((((((triple1) -> rule1)) -> rule6) ((triple2) -> rule7)) -> rule3) OR ((((((triple2) -> rule7)) -> rule6) ((triple1) -> rule1)) -> rule3) OR ((((((triple2) -> rule7)) -> rule6) ((triple2) -> rule7)) -> rule3))]
The dog eats the lion.
("dog" "eats" "lion" "+")
triple1
The lion eats the dog.
("lion" "eats" "dog" "+")
triple2
The dog is blue.
("dog" "is" "blue" "+")
((triple1) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
((triple2) -> (rule7 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog does not chase the dog.
("dog" "chases" "dog" "-")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2)) ((triple1) -> (rule1 % int3))) -> (rule3 % int1))
The dog does not chase the dog.
("dog" "chases" "dog" "-")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2)) ((triple2) -> (rule7 % int3))) -> (rule3 % int1))
The dog does not chase the dog.
("dog" "chases" "dog" "-")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
((((((triple2) -> (rule7 % int3))) -> (rule6 % int2)) ((triple1) -> (rule1 % int3))) -> (rule3 % int1))
The dog does not chase the dog.
("dog" "chases" "dog" "-")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
((((((triple2) -> (rule7 % int3))) -> (rule6 % int2)) ((triple2) -> (rule7 % int3))) -> (rule3 % int1))
The dog does not chase the dog.
("dog" "chases" "dog" "-")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3