The bald eagle is rough. The bald eagle likes the cat. The bald eagle likes the dog. The bald eagle sees the lion. The cat is big. The cat needs the bald eagle. The cat needs the dog. The dog is big. The dog is cold. The dog is young. The dog needs the cat. The dog sees the cat. The lion likes the cat. The lion needs the bald eagle. If something is rough then it is young. If something sees the bald eagle then the bald eagle likes the dog. If something likes the dog and the dog sees the lion then the lion likes the cat. If something needs the dog then it sees the cat. If something is young then it needs the lion. If the bald eagle needs the lion then the lion is rough. If the lion is young and the lion is big then the lion needs the bald eagle. If something likes the dog and it is kind then the dog needs the lion.
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
The bald eagle likes the cat.
("bald eagle" "likes" "cat" "+")
The bald eagle likes the dog.
("bald eagle" "likes" "dog" "+")
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
The cat is big.
("cat" "is" "big" "+")
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
If something is rough then it is young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something sees the bald eagle then the bald eagle likes the dog.
((("something" "sees" "bald eagle" "+")) -> ("bald eagle" "likes" "dog" "+"))
If something likes the dog and the dog sees the lion then the lion likes the cat.
((("something" "likes" "dog" "+") ("dog" "sees" "lion" "+")) -> ("lion" "likes" "cat" "+"))
If something needs the dog then it sees the cat.
((("something" "needs" "dog" "+")) -> ("something" "sees" "cat" "+"))
If something is young then it needs the lion.
((("something" "is" "young" "+")) -> ("something" "needs" "lion" "+"))
If the bald eagle needs the lion then the lion is rough.
((("bald eagle" "needs" "lion" "+")) -> ("lion" "is" "rough" "+"))
If the lion is young and the lion is big then the lion needs the bald eagle.
((("lion" "is" "young" "+") ("lion" "is" "big" "+")) -> ("lion" "needs" "bald eagle" "+"))
If something likes the dog and it is kind then the dog needs the lion.
((("something" "likes" "dog" "+") ("something" "is" "kind" "+")) -> ("dog" "needs" "lion" "+"))
The bald eagle likes the dog.
True
1
proof
[(triple3)]
("bald eagle" "likes" "dog" "+")
triple3
The dog is not big.
False
1
inv-proof
[(triple8)]
("dog" "is" "big" "-")
triple8
The dog needs the lion.
True
2
proof
[(((triple10) -> rule5))]
("dog" "needs" "lion" "+")
((triple10) -> (rule5 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The cat does not see the cat.
False
2
inv-proof
[(((triple7) -> rule4))]
("cat" "sees" "cat" "-")
((triple7) -> (rule4 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The bald eagle needs the lion.
True
3
proof
[(((((triple1) -> rule1)) -> rule5))]
("bald eagle" "needs" "lion" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2
The bald eagle does not need the lion.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule5))]
("bald eagle" "needs" "lion" "-")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2
The lion is rough.
True
4
proof
[(((((((triple1) -> rule1)) -> rule5)) -> rule6))]
("lion" "is" "rough" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int2
The bald eagle is young.
("bald eagle" "is" "young" "+")
int3
The lion is not rough.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule5)) -> rule6))]
("lion" "is" "rough" "-")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int2
The bald eagle is young.
("bald eagle" "is" "young" "+")
int3
The lion is young.
True
5
proof
[(((((((((triple1) -> rule1)) -> rule5)) -> rule6)) -> rule1))]
("lion" "is" "young" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int3
The bald eagle is young.
("bald eagle" "is" "young" "+")
int4
The lion is not young.
False
5
inv-proof
[(((((((((triple1) -> rule1)) -> rule5)) -> rule6)) -> rule1))]
("lion" "is" "young" "-")
((((((((triple1) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int3
The bald eagle is young.
("bald eagle" "is" "young" "+")
int4
The lion needs the lion.
True
6
proof
[(((((((((((triple1) -> rule1)) -> rule5)) -> rule6)) -> rule1)) -> rule5))]
("lion" "needs" "lion" "+")
((((((((((triple1) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int4
The bald eagle is young.
("bald eagle" "is" "young" "+")
int5
The lion does not need the lion.
False
6
inv-proof
[(((((((((((triple1) -> rule1)) -> rule5)) -> rule6)) -> rule1)) -> rule5))]
("lion" "needs" "lion" "-")
((((((((((triple1) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int4
The bald eagle is young.
("bald eagle" "is" "young" "+")
int5
The cat does not need the lion.
Unknown
inv-rconc
[@2: The cat needs the lion.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("cat" "needs" "lion" "-")
The cat is young.
Unknown
rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "young" "+")
The bald eagle does not see the cat.
Unknown
inv-rconc
[@1: The bald eagle sees the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bald eagle" "sees" "cat" "-")
The lion sees the cat.
Unknown
rconc
[@1: The lion sees the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "sees" "cat" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The lion needs the cat.
Unknown
random
[@0: The lion needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "cat" "+")
The cat is not rough.
Unknown
inv-random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "-")
The lion is big.
Unknown
random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "+")
The lion does not like the bald eagle.
Unknown
inv-random
[@0: The lion likes the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "bald eagle" "-")
The cat likes the dog.
Unknown
random
[@0: The cat likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "dog" "+")
The cat does not see the bald eagle.
Unknown
inv-random
[@0: The cat sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "bald eagle" "-")
The dog likes the cat.
Unknown
random
[@0: The dog likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "cat" "+")
@0: The bald eagle is rough.[(triple1)] The bald eagle likes the cat.[(triple2)] The bald eagle likes the dog.[(triple3)] The bald eagle sees the lion.[(triple4)] The cat is big.[(triple5)] The cat needs the bald eagle.[(triple6)] The cat needs the dog.[(triple7)] The dog is big.[(triple8)] The dog is cold.[(triple9)] The dog is young.[(triple10)] The dog needs the cat.[(triple11)] The dog sees the cat.[(triple12)] The lion likes the cat.[(triple13)] The lion needs the bald eagle.[(triple14)] @1: The bald eagle is young.[(((triple1) -> rule1))] The cat sees the cat.[(((triple7) -> rule4))] The dog needs the lion.[(((triple10) -> rule5))] @2: The bald eagle needs the lion.[(((((triple1) -> rule1)) -> rule5))] @3: The lion is rough.[(((((((triple1) -> rule1)) -> rule5)) -> rule6))] @4: The lion is young.[(((((((((triple1) -> rule1)) -> rule5)) -> rule6)) -> rule1))] @5: The lion needs the lion.[(((((((((((triple1) -> rule1)) -> rule5)) -> rule6)) -> rule1)) -> rule5))]
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
triple1
The bald eagle likes the cat.
("bald eagle" "likes" "cat" "+")
triple2
The bald eagle likes the dog.
("bald eagle" "likes" "dog" "+")
triple3
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
triple4
The cat is big.
("cat" "is" "big" "+")
triple5
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
triple6
The cat needs the dog.
("cat" "needs" "dog" "+")
triple7
The dog is big.
("dog" "is" "big" "+")
triple8
The dog is cold.
("dog" "is" "cold" "+")
triple9
The dog is young.
("dog" "is" "young" "+")
triple10
The dog needs the cat.
("dog" "needs" "cat" "+")
triple11
The dog sees the cat.
("dog" "sees" "cat" "+")
triple12
The lion likes the cat.
("lion" "likes" "cat" "+")
triple13
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
triple14
The bald eagle is young.
("bald eagle" "is" "young" "+")
((triple1) -> (rule1 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple7) -> (rule4 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
((triple10) -> (rule5 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int2
The bald eagle is young.
("bald eagle" "is" "young" "+")
int3
The lion is young.
("lion" "is" "young" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int3
The bald eagle is young.
("bald eagle" "is" "young" "+")
int4
The lion needs the lion.
("lion" "needs" "lion" "+")
((((((((((triple1) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int4
The bald eagle is young.
("bald eagle" "is" "young" "+")
int5