The cat likes the lion. The cat needs the cow. The cow eats the cat. The cow is kind. The cow likes the dog. The cow likes the lion. The cow needs the dog. The dog eats the cow. The dog likes the cow. The lion likes the dog. If something is round and it needs the cat then it is nice. If the cat is nice then the cat likes the lion. If something is round then it eats the lion. If something needs the cat then the cat likes the lion. All young things are round. If something is round then it needs the lion. If something likes the cow then the cow is young. If the cow eats the lion and the cow needs the dog then the lion is round.
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow likes the dog.
("cow" "likes" "dog" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
The dog likes the cow.
("dog" "likes" "cow" "+")
The lion likes the dog.
("lion" "likes" "dog" "+")
If something is round and it needs the cat then it is nice.
((("something" "is" "round" "+") ("something" "needs" "cat" "+")) -> ("something" "is" "nice" "+"))
If the cat is nice then the cat likes the lion.
((("cat" "is" "nice" "+")) -> ("cat" "likes" "lion" "+"))
If something is round then it eats the lion.
((("something" "is" "round" "+")) -> ("something" "eats" "lion" "+"))
If something needs the cat then the cat likes the lion.
((("something" "needs" "cat" "+")) -> ("cat" "likes" "lion" "+"))
All young things are round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
If something is round then it needs the lion.
((("something" "is" "round" "+")) -> ("something" "needs" "lion" "+"))
If something likes the cow then the cow is young.
((("something" "likes" "cow" "+")) -> ("cow" "is" "young" "+"))
If the cow eats the lion and the cow needs the dog then the lion is round.
((("cow" "eats" "lion" "+") ("cow" "needs" "dog" "+")) -> ("lion" "is" "round" "+"))
The lion likes the dog.
True
1
proof
[(triple10)]
("lion" "likes" "dog" "+")
triple10
The cow is not kind.
False
1
inv-proof
[(triple4)]
("cow" "is" "kind" "-")
triple4
The cow is young.
True
2
proof
[(((triple9) -> rule7))]
("cow" "is" "young" "+")
((triple9) -> (rule7 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is not young.
False
2
inv-proof
[(((triple9) -> rule7))]
("cow" "is" "young" "-")
((triple9) -> (rule7 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is round.
True
3
proof
[(((((triple9) -> rule7)) -> rule5))]
("cow" "is" "round" "+")
((((triple9) -> (rule7 % int2))) -> (rule5 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is not round.
False
3
inv-proof
[(((((triple9) -> rule7)) -> rule5))]
("cow" "is" "round" "-")
((((triple9) -> (rule7 % int2))) -> (rule5 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow eats the lion.
True
4
proof
[(((((((triple9) -> rule7)) -> rule5)) -> rule3))]
("cow" "eats" "lion" "+")
((((((triple9) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The cow is young.
("cow" "is" "young" "+")
int3
The cow does not eat the lion.
False
4
inv-proof
[(((((((triple9) -> rule7)) -> rule5)) -> rule3))]
("cow" "eats" "lion" "-")
((((((triple9) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The cow is young.
("cow" "is" "young" "+")
int3
The lion is round.
True
6
proof
[(((((((((triple9) -> rule7)) -> rule5)) -> rule3) triple7) -> rule8))]
("lion" "is" "round" "+")
((((((((triple9) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) triple7) -> (rule8 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3
The cow is young.
("cow" "is" "young" "+")
int4
The lion is not round.
False
6
inv-proof
[(((((((((triple9) -> rule7)) -> rule5)) -> rule3) triple7) -> rule8))]
("lion" "is" "round" "-")
((((((((triple9) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) triple7) -> (rule8 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3
The cow is young.
("cow" "is" "young" "+")
int4
The lion eats the lion.
True
7
proof
[(((((((((((triple9) -> rule7)) -> rule5)) -> rule3) triple7) -> rule8)) -> rule3))]
("lion" "eats" "lion" "+")
((((((((((triple9) -> (rule7 % int5))) -> (rule5 % int4))) -> (rule3 % int3)) triple7) -> (rule8 % int2))) -> (rule3 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The cow eats the lion.
("cow" "eats" "lion" "+")
int3
The cow is round.
("cow" "is" "round" "+")
int4
The cow is young.
("cow" "is" "young" "+")
int5
The lion does not eat the lion.
False
7
inv-proof
[(((((((((((triple9) -> rule7)) -> rule5)) -> rule3) triple7) -> rule8)) -> rule3))]
("lion" "eats" "lion" "-")
((((((((((triple9) -> (rule7 % int5))) -> (rule5 % int4))) -> (rule3 % int3)) triple7) -> (rule8 % int2))) -> (rule3 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The cow eats the lion.
("cow" "eats" "lion" "+")
int3
The cow is round.
("cow" "is" "round" "+")
int4
The cow is young.
("cow" "is" "young" "+")
int5
The dog is not round.
Unknown
inv-rconc
[@1: The dog is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "round" "-")
The dog eats the lion.
Unknown
rconc
[@2: The dog eats the lion.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("dog" "eats" "lion" "+")
The cat does not need the lion.
Unknown
inv-rconc
[@2: The cat needs the lion.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("cat" "needs" "lion" "-")
The lion is nice.
Unknown
rconc
[@1: The lion is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "nice" "+")
The dog is not nice.
Unknown
inv-rconc
[@1: The dog is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "nice" "-")
The dog needs the lion.
Unknown
rconc
[@2: The dog needs the lion.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("dog" "needs" "lion" "+")
The lion is not young.
Unknown
inv-random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The lion eats the cow.
Unknown
random
[@0: The lion eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "cow" "+")
The dog does not eat the cat.
Unknown
inv-random
[@0: The dog eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "cat" "-")
The cat likes the dog.
Unknown
random
[@0: The cat likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "dog" "+")
@0: The cat likes the lion.[(triple1)] The cat needs the cow.[(triple2)] The cow eats the cat.[(triple3)] The cow is kind.[(triple4)] The cow likes the dog.[(triple5)] The cow likes the lion.[(triple6)] The cow needs the dog.[(triple7)] The dog eats the cow.[(triple8)] The dog likes the cow.[(triple9)] The lion likes the dog.[(triple10)] @1: The cow is young.[(((triple9) -> rule7))] @2: The cow is round.[(((((triple9) -> rule7)) -> rule5))] @3: The cow eats the lion.[(((((((triple9) -> rule7)) -> rule5)) -> rule3))] The cow needs the lion.[(((((((triple9) -> rule7)) -> rule5)) -> rule6))] @4: The lion is round.[(((((((((triple9) -> rule7)) -> rule5)) -> rule3) triple7) -> rule8))] @5: The lion eats the lion.[(((((((((((triple9) -> rule7)) -> rule5)) -> rule3) triple7) -> rule8)) -> rule3))] The lion needs the lion.[(((((((((((triple9) -> rule7)) -> rule5)) -> rule3) triple7) -> rule8)) -> rule6))]
The cat likes the lion.
("cat" "likes" "lion" "+")
triple1
The cat needs the cow.
("cat" "needs" "cow" "+")
triple2
The cow eats the cat.
("cow" "eats" "cat" "+")
triple3
The cow is kind.
("cow" "is" "kind" "+")
triple4
The cow likes the dog.
("cow" "likes" "dog" "+")
triple5
The cow likes the lion.
("cow" "likes" "lion" "+")
triple6
The cow needs the dog.
("cow" "needs" "dog" "+")
triple7
The dog eats the cow.
("dog" "eats" "cow" "+")
triple8
The dog likes the cow.
("dog" "likes" "cow" "+")
triple9
The lion likes the dog.
("lion" "likes" "dog" "+")
triple10
The cow is young.
("cow" "is" "young" "+")
((triple9) -> (rule7 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is round.
("cow" "is" "round" "+")
((((triple9) -> (rule7 % int2))) -> (rule5 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow eats the lion.
("cow" "eats" "lion" "+")
((((((triple9) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The cow is young.
("cow" "is" "young" "+")
int3
The cow needs the lion.
("cow" "needs" "lion" "+")
((((((triple9) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cow needs the lion.
("cow" "needs" "lion" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The cow is young.
("cow" "is" "young" "+")
int3
The lion is round.
("lion" "is" "round" "+")
((((((((triple9) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) triple7) -> (rule8 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3
The cow is young.
("cow" "is" "young" "+")
int4
The lion eats the lion.
("lion" "eats" "lion" "+")
((((((((((triple9) -> (rule7 % int5))) -> (rule5 % int4))) -> (rule3 % int3)) triple7) -> (rule8 % int2))) -> (rule3 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The cow eats the lion.
("cow" "eats" "lion" "+")
int3
The cow is round.
("cow" "is" "round" "+")
int4
The cow is young.
("cow" "is" "young" "+")
int5
The lion needs the lion.
("lion" "needs" "lion" "+")
((((((((((triple9) -> (rule7 % int5))) -> (rule5 % int4))) -> (rule3 % int3)) triple7) -> (rule8 % int2))) -> (rule6 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The cow eats the lion.
("cow" "eats" "lion" "+")
int3
The cow is round.
("cow" "is" "round" "+")
int4
The cow is young.
("cow" "is" "young" "+")
int5