The dog eats the lion. The dog is red. The dog is young. The dog visits the lion. The lion chases the dog. The lion eats the dog. The lion is rough. The lion is round. The lion is young. The lion visits the dog. If someone is red and they chase the dog then they do not eat the lion. If someone visits the lion and the lion does not chase the dog then they eat the lion. If someone visits the dog then they are round. If someone eats the dog then they are big. If someone is big then they are red. If someone eats the lion then the lion is big.
The dog eats the lion.
("dog" "eats" "lion" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is young.
("dog" "is" "young" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is round.
("lion" "is" "round" "+")
The lion is young.
("lion" "is" "young" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
If someone is red and they chase the dog then they do not eat the lion.
((("someone" "is" "red" "+") ("someone" "chases" "dog" "+")) -> ("someone" "eats" "lion" "-"))
If someone visits the lion and the lion does not chase the dog then they eat the lion.
((("someone" "visits" "lion" "+") ("lion" "chases" "dog" "~")) -> ("someone" "eats" "lion" "+"))
If someone visits the dog then they are round.
((("someone" "visits" "dog" "+")) -> ("someone" "is" "round" "+"))
If someone eats the dog then they are big.
((("someone" "eats" "dog" "+")) -> ("someone" "is" "big" "+"))
If someone is big then they are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
If someone eats the lion then the lion is big.
((("someone" "eats" "lion" "+")) -> ("lion" "is" "big" "+"))
The dog visits the lion.
True
1
proof
[(triple4)]
("dog" "visits" "lion" "+")
triple4
The lion does not eat the dog.
False
1
inv-proof
[(triple6)]
("lion" "eats" "dog" "-")
triple6
The lion is big.
True
2
proof
[(((triple1) -> rule6) OR ((triple6) -> rule4))]
("lion" "is" "big" "+")
((triple1) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
((triple6) -> (rule4 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is not big.
False
2
inv-proof
[(((triple1) -> rule6) OR ((triple6) -> rule4))]
("lion" "is" "big" "-")
((triple1) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
((triple6) -> (rule4 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is red.
True
3
proof
[(((((triple1) -> rule6)) -> rule5) OR ((((triple6) -> rule4)) -> rule5))]
("lion" "is" "red" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
((((triple6) -> (rule4 % int2))) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion is not red.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule5) OR ((((triple6) -> rule4)) -> rule5))]
("lion" "is" "red" "-")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
((((triple6) -> (rule4 % int2))) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion does not eat the lion.
True
5
proof
[(((((((triple1) -> rule6)) -> rule5) triple5) -> rule1) OR ((((((triple6) -> rule4)) -> rule5) triple5) -> rule1))]
("lion" "eats" "lion" "-")
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2)) triple5) -> (rule1 % int1))
The lion does not eat the lion.
("lion" "eats" "lion" "-")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
((((((triple6) -> (rule4 % int3))) -> (rule5 % int2)) triple5) -> (rule1 % int1))
The lion does not eat the lion.
("lion" "eats" "lion" "-")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The lion eats the lion.
False
5
inv-proof
[(((((((triple1) -> rule6)) -> rule5) triple5) -> rule1) OR ((((((triple6) -> rule4)) -> rule5) triple5) -> rule1))]
("lion" "eats" "lion" "+")
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2)) triple5) -> (rule1 % int1))
The lion does not eat the lion.
("lion" "eats" "lion" "-")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
((((((triple6) -> (rule4 % int3))) -> (rule5 % int2)) triple5) -> (rule1 % int1))
The lion does not eat the lion.
("lion" "eats" "lion" "-")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The dog is not round.
Unknown
inv-rconc
[@1: The dog is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "round" "-")
The dog is big.
Unknown
rconc
[@1: The dog is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "is" "big" "+")
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 is rough.
Unknown
random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "+")
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
The lion does not visit the lion.
Unknown
inv-random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "-")
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 eats the lion.[(triple1)] The dog is red.[(triple2)] The dog is young.[(triple3)] The dog visits the lion.[(triple4)] The lion chases the dog.[(triple5)] The lion eats the dog.[(triple6)] The lion is rough.[(triple7)] The lion is round.[(triple8 OR ((triple10) -> rule3))] The lion is young.[(triple9)] The lion visits the dog.[(triple10)] @1: The lion is big.[(((triple1) -> rule6) OR ((triple6) -> rule4))] @2: The lion is red.[(((((triple1) -> rule6)) -> rule5) OR ((((triple6) -> rule4)) -> rule5))] @3: The lion does not eat the lion.[(((((((triple1) -> rule6)) -> rule5) triple5) -> rule1) OR ((((((triple6) -> rule4)) -> rule5) triple5) -> rule1))]
The dog eats the lion.
("dog" "eats" "lion" "+")
triple1
The dog is red.
("dog" "is" "red" "+")
triple2
The dog is young.
("dog" "is" "young" "+")
triple3
The dog visits the lion.
("dog" "visits" "lion" "+")
triple4
The lion chases the dog.
("lion" "chases" "dog" "+")
triple5
The lion eats the dog.
("lion" "eats" "dog" "+")
triple6
The lion is rough.
("lion" "is" "rough" "+")
triple7
The lion is round.
("lion" "is" "round" "+")
triple8
((triple10) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is young.
("lion" "is" "young" "+")
triple9
The lion visits the dog.
("lion" "visits" "dog" "+")
triple10
The lion is big.
("lion" "is" "big" "+")
((triple1) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
((triple6) -> (rule4 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is red.
("lion" "is" "red" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
((((triple6) -> (rule4 % int2))) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion does not eat the lion.
("lion" "eats" "lion" "-")
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2)) triple5) -> (rule1 % int1))
The lion does not eat the lion.
("lion" "eats" "lion" "-")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
((((((triple6) -> (rule4 % int3))) -> (rule5 % int2)) triple5) -> (rule1 % int1))
The lion does not eat the lion.
("lion" "eats" "lion" "-")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3