The cow likes the lion. The dog chases the lion. The dog likes the cow. The dog likes the lion. The dog needs the cow. The dog needs the lion. The lion is big. If someone likes the lion then they need the cow. If someone chases the lion then they are not cold. If the lion is young then the lion does not like the dog. If the lion is big and the lion chases the cow then the lion needs the dog. If someone likes the lion then the lion chases the cow. If the lion needs the dog then the lion is young.
The cow likes the lion.
("cow" "likes" "lion" "+")
The dog chases the lion.
("dog" "chases" "lion" "+")
The dog likes the cow.
("dog" "likes" "cow" "+")
The dog likes the lion.
("dog" "likes" "lion" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The lion is big.
("lion" "is" "big" "+")
If someone likes the lion then they need the cow.
((("someone" "likes" "lion" "+")) -> ("someone" "needs" "cow" "+"))
If someone chases the lion then they are not cold.
((("someone" "chases" "lion" "+")) -> ("someone" "is" "cold" "-"))
If the lion is young then the lion does not like the dog.
((("lion" "is" "young" "+")) -> ("lion" "likes" "dog" "-"))
If the lion is big and the lion chases the cow then the lion needs the dog.
((("lion" "is" "big" "+") ("lion" "chases" "cow" "+")) -> ("lion" "needs" "dog" "+"))
If someone likes the lion then the lion chases the cow.
((("someone" "likes" "lion" "+")) -> ("lion" "chases" "cow" "+"))
If the lion needs the dog then the lion is young.
((("lion" "needs" "dog" "+")) -> ("lion" "is" "young" "+"))
The lion is big.
True
1
proof
[(triple7)]
("lion" "is" "big" "+")
triple7
The lion is not big.
False
1
inv-proof
[(triple7)]
("lion" "is" "big" "-")
triple7
The dog is not cold.
True
2
proof
[(((triple2) -> rule2))]
("dog" "is" "cold" "-")
((triple2) -> (rule2 % int1))
The dog is not cold.
("dog" "is" "cold" "-")
int1
The lion does not chase the cow.
False
2
inv-proof
[(((triple1) -> rule5) OR ((triple4) -> rule5))]
("lion" "chases" "cow" "-")
((triple1) -> (rule5 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
((triple4) -> (rule5 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The lion needs the dog.
True
4
proof
[(((triple7 ((triple1) -> rule5)) -> rule4) OR ((triple7 ((triple4) -> rule5)) -> rule4))]
("lion" "needs" "dog" "+")
((triple7 ((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2
((triple7 ((triple4) -> (rule5 % int2))) -> (rule4 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2
The lion does not need the dog.
False
4
inv-proof
[(((triple7 ((triple1) -> rule5)) -> rule4) OR ((triple7 ((triple4) -> rule5)) -> rule4))]
("lion" "needs" "dog" "-")
((triple7 ((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2
((triple7 ((triple4) -> (rule5 % int2))) -> (rule4 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2
The lion is young.
True
5
proof
[(((((triple7 ((triple1) -> rule5)) -> rule4)) -> rule6) OR ((((triple7 ((triple4) -> rule5)) -> rule4)) -> rule6))]
("lion" "is" "young" "+")
((((triple7 ((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
int2
The lion chases the cow.
("lion" "chases" "cow" "+")
int3
((((triple7 ((triple4) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
int2
The lion chases the cow.
("lion" "chases" "cow" "+")
int3
The lion is not young.
False
5
inv-proof
[(((((triple7 ((triple1) -> rule5)) -> rule4)) -> rule6) OR ((((triple7 ((triple4) -> rule5)) -> rule4)) -> rule6))]
("lion" "is" "young" "-")
((((triple7 ((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
int2
The lion chases the cow.
("lion" "chases" "cow" "+")
int3
((((triple7 ((triple4) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
int2
The lion chases the cow.
("lion" "chases" "cow" "+")
int3
The lion does not need the cow.
Unknown
inv-rconc
[@1: The lion needs the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "needs" "cow" "-")
The lion likes the cow.
Unknown
random
[@0: The lion likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "cow" "+")
The dog is not young.
Unknown
inv-random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "-")
The cow is big.
Unknown
random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "+")
The cow does not chase the dog.
Unknown
inv-random
[@0: The cow chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "dog" "-")
The lion is nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
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 big.
Unknown
random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "+")
@0: The cow likes the lion.[(triple1)] The dog chases the lion.[(triple2)] The dog likes the cow.[(triple3)] The dog likes the lion.[(triple4)] The dog needs the cow.[(triple5 OR ((triple4) -> rule1))] The dog needs the lion.[(triple6)] The lion is big.[(triple7)] @1: The cow needs the cow.[(((triple1) -> rule1))] The dog is not cold.[(((triple2) -> rule2))] The lion chases the cow.[(((triple1) -> rule5) OR ((triple4) -> rule5))] @2: The lion needs the dog.[(((triple7 ((triple1) -> rule5)) -> rule4) OR ((triple7 ((triple4) -> rule5)) -> rule4))] @3: The lion is young.[(((((triple7 ((triple1) -> rule5)) -> rule4)) -> rule6) OR ((((triple7 ((triple4) -> rule5)) -> rule4)) -> rule6))] @4: The lion does not like the dog.[(((((((triple7 ((triple1) -> rule5)) -> rule4)) -> rule6)) -> rule3) OR ((((((triple7 ((triple4) -> rule5)) -> rule4)) -> rule6)) -> rule3))]
The cow likes the lion.
("cow" "likes" "lion" "+")
triple1
The dog chases the lion.
("dog" "chases" "lion" "+")
triple2
The dog likes the cow.
("dog" "likes" "cow" "+")
triple3
The dog likes the lion.
("dog" "likes" "lion" "+")
triple4
The dog needs the cow.
("dog" "needs" "cow" "+")
triple5
((triple4) -> (rule1 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
triple6
The lion is big.
("lion" "is" "big" "+")
triple7
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple1) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The dog is not cold.
("dog" "is" "cold" "-")
((triple2) -> (rule2 % int1))
The dog is not cold.
("dog" "is" "cold" "-")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
((triple1) -> (rule5 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
((triple4) -> (rule5 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
((triple7 ((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2
((triple7 ((triple4) -> (rule5 % int2))) -> (rule4 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2
The lion is young.
("lion" "is" "young" "+")
((((triple7 ((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
int2
The lion chases the cow.
("lion" "chases" "cow" "+")
int3
((((triple7 ((triple4) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
int2
The lion chases the cow.
("lion" "chases" "cow" "+")
int3
The lion does not like the dog.
("lion" "likes" "dog" "-")
((((((triple7 ((triple1) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion does not like the dog.
("lion" "likes" "dog" "-")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion needs the dog.
("lion" "needs" "dog" "+")
int3
The lion chases the cow.
("lion" "chases" "cow" "+")
int4
((((((triple7 ((triple4) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion does not like the dog.
("lion" "likes" "dog" "-")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion needs the dog.
("lion" "needs" "dog" "+")
int3
The lion chases the cow.
("lion" "chases" "cow" "+")
int4