The dog is big. The dog is kind. The dog is round. The dog needs the lion. The lion does not chase the dog. The lion eats the dog. The lion is green. If someone needs the dog and the dog does not chase the lion then the dog does not eat the lion. If someone eats the lion then the lion is green. If someone needs the lion and the lion does not eat the dog then the lion needs the dog. If someone eats the dog and the dog needs the lion then they eat the lion. If someone is blue and they need the lion then the lion does not chase the dog. If someone eats the lion then they need the dog.
The dog is big.
("dog" "is" "big" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is round.
("dog" "is" "round" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The lion does not chase the dog.
("lion" "chases" "dog" "-")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion is green.
("lion" "is" "green" "+")
If someone needs the dog and the dog does not chase the lion then the dog does not eat the lion.
((("someone" "needs" "dog" "+") ("dog" "chases" "lion" "~")) -> ("dog" "eats" "lion" "-"))
If someone eats the lion then the lion is green.
((("someone" "eats" "lion" "+")) -> ("lion" "is" "green" "+"))
If someone needs the lion and the lion does not eat the dog then the lion needs the dog.
((("someone" "needs" "lion" "+") ("lion" "eats" "dog" "~")) -> ("lion" "needs" "dog" "+"))
If someone eats the dog and the dog needs the lion then they eat the lion.
((("someone" "eats" "dog" "+") ("dog" "needs" "lion" "+")) -> ("someone" "eats" "lion" "+"))
If someone is blue and they need the lion then the lion does not chase the dog.
((("someone" "is" "blue" "+") ("someone" "needs" "lion" "+")) -> ("lion" "chases" "dog" "-"))
If someone eats the lion then they need the dog.
((("someone" "eats" "lion" "+")) -> ("someone" "needs" "dog" "+"))
The dog is kind.
True
1
proof
[(triple2)]
("dog" "is" "kind" "+")
triple2
The lion is not green.
False
1
inv-proof
[(triple7 OR ((((triple6 triple4) -> rule4)) -> rule2))]
("lion" "is" "green" "-")
triple7
((((triple6 triple4) -> (rule4 % int2))) -> (rule2 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion eats the lion.
True
3
proof
[(((triple6 triple4) -> rule4))]
("lion" "eats" "lion" "+")
((triple6 triple4) -> (rule4 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion does not eat the lion.
False
3
inv-proof
[(((triple6 triple4) -> rule4))]
("lion" "eats" "lion" "-")
((triple6 triple4) -> (rule4 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion needs the dog.
True
4
proof
[(((((triple6 triple4) -> rule4)) -> rule6))]
("lion" "needs" "dog" "+")
((((triple6 triple4) -> (rule4 % int2))) -> (rule6 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion does not need the dog.
False
4
inv-proof
[(((((triple6 triple4) -> rule4)) -> rule6))]
("lion" "needs" "dog" "-")
((((triple6 triple4) -> (rule4 % int2))) -> (rule6 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The dog does not eat the lion.
Unknown
inv-rconc
[@1: The dog eats the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "eats" "lion" "-")
The dog needs the dog.
Unknown
rconc
[@2: The dog needs the dog.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("dog" "needs" "dog" "+")
The dog is not blue.
Unknown
inv-random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
@0: The dog is big.[(triple1)] The dog is kind.[(triple2)] The dog is round.[(triple3)] The dog needs the lion.[(triple4)] The lion does not chase the dog.[(triple5)] The lion eats the dog.[(triple6)] The lion is green.[(triple7 OR ((((triple6 triple4) -> rule4)) -> rule2))] @1: The lion eats the lion.[(((triple6 triple4) -> rule4))] @2: The lion needs the dog.[(((((triple6 triple4) -> rule4)) -> rule6))]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog is kind.
("dog" "is" "kind" "+")
triple2
The dog is round.
("dog" "is" "round" "+")
triple3
The dog needs the lion.
("dog" "needs" "lion" "+")
triple4
The lion does not chase the dog.
("lion" "chases" "dog" "-")
triple5
The lion eats the dog.
("lion" "eats" "dog" "+")
triple6
The lion is green.
("lion" "is" "green" "+")
triple7
((((triple6 triple4) -> (rule4 % int2))) -> (rule2 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion eats the lion.
("lion" "eats" "lion" "+")
((triple6 triple4) -> (rule4 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
((((triple6 triple4) -> (rule4 % int2))) -> (rule6 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2