The bald eagle is cold. The bald eagle is young. The bald eagle sees the tiger. The cat sees the tiger. The lion does not like the tiger. The tiger is cold. The tiger does not see the cat. If something sees the tiger then it sees the bald eagle. If the lion sees the bald eagle then the bald eagle does not like the tiger. If something sees the bald eagle then the bald eagle sees the lion. If something is nice and young then it needs the tiger. If the bald eagle likes the lion then the lion does not see the tiger. If something sees the bald eagle and it sees the lion then the lion sees the tiger. If something is young and it likes the tiger then it likes the bald eagle. If something sees the bald eagle and it is not nice then it is round. If something is nice and it does not see the tiger then the tiger likes the cat.
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
The bald eagle is young.
("bald eagle" "is" "young" "+")
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The lion does not like the tiger.
("lion" "likes" "tiger" "-")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger does not see the cat.
("tiger" "sees" "cat" "-")
If something sees the tiger then it sees the bald eagle.
((("something" "sees" "tiger" "+")) -> ("something" "sees" "bald eagle" "+"))
If the lion sees the bald eagle then the bald eagle does not like the tiger.
((("lion" "sees" "bald eagle" "+")) -> ("bald eagle" "likes" "tiger" "-"))
If something sees the bald eagle then the bald eagle sees the lion.
((("something" "sees" "bald eagle" "+")) -> ("bald eagle" "sees" "lion" "+"))
If something is nice and young then it needs the tiger.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "needs" "tiger" "+"))
If the bald eagle likes the lion then the lion does not see the tiger.
((("bald eagle" "likes" "lion" "+")) -> ("lion" "sees" "tiger" "-"))
If something sees the bald eagle and it sees the lion then the lion sees the tiger.
((("something" "sees" "bald eagle" "+") ("something" "sees" "lion" "+")) -> ("lion" "sees" "tiger" "+"))
If something is young and it likes the tiger then it likes the bald eagle.
((("something" "is" "young" "+") ("something" "likes" "tiger" "+")) -> ("something" "likes" "bald eagle" "+"))
If something sees the bald eagle and it is not nice then it is round.
((("something" "sees" "bald eagle" "+") ("something" "is" "nice" "~")) -> ("something" "is" "round" "+"))
If something is nice and it does not see the tiger then the tiger likes the cat.
((("something" "is" "nice" "+") ("something" "sees" "tiger" "~")) -> ("tiger" "likes" "cat" "+"))
The tiger is cold.
True
1
proof
[(triple6)]
("tiger" "is" "cold" "+")
triple6
The tiger is not cold.
False
1
inv-proof
[(triple6)]
("tiger" "is" "cold" "-")
triple6
The cat sees the bald eagle.
True
2
proof
[(((triple4) -> rule1))]
("cat" "sees" "bald eagle" "+")
((triple4) -> (rule1 % int1))
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int1
The bald eagle does not see the bald eagle.
False
2
inv-proof
[(((triple3) -> rule1))]
("bald eagle" "sees" "bald eagle" "-")
((triple3) -> (rule1 % int1))
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int1
The bald eagle sees the lion.
True
3
proof
[(((((triple3) -> rule1)) -> rule3) OR ((((triple4) -> rule1)) -> rule3))]
("bald eagle" "sees" "lion" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int1
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int2
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int2
The bald eagle does not see the lion.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule3) OR ((((triple4) -> rule1)) -> rule3))]
("bald eagle" "sees" "lion" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int1
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int2
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int2
The lion sees the tiger.
True
6
proof
[(((((triple3) -> rule1) ((((triple3) -> rule1)) -> rule3)) -> rule6) OR ((((triple3) -> rule1) ((((triple4) -> rule1)) -> rule3)) -> rule6))]
("lion" "sees" "tiger" "+")
((((triple3) -> (rule1 % int3)) ((((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int2
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int3
((((triple3) -> (rule1 % int4)) ((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int2
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int3
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int4
The lion does not see the tiger.
False
6
inv-proof
[(((((triple3) -> rule1) ((((triple3) -> rule1)) -> rule3)) -> rule6) OR ((((triple3) -> rule1) ((((triple4) -> rule1)) -> rule3)) -> rule6))]
("lion" "sees" "tiger" "-")
((((triple3) -> (rule1 % int3)) ((((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int2
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int3
((((triple3) -> (rule1 % int4)) ((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int2
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int3
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int4
The lion sees the bald eagle.
True
7
proof
[(((((((triple3) -> rule1) ((((triple3) -> rule1)) -> rule3)) -> rule6)) -> rule1) OR ((((((triple3) -> rule1) ((((triple4) -> rule1)) -> rule3)) -> rule6)) -> rule1))]
("lion" "sees" "bald eagle" "+")
((((((triple3) -> (rule1 % int4)) ((((triple3) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int3
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int4
((((((triple3) -> (rule1 % int5)) ((((triple4) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int3
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int4
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int5
The lion does not see the bald eagle.
False
7
inv-proof
[(((((((triple3) -> rule1) ((((triple3) -> rule1)) -> rule3)) -> rule6)) -> rule1) OR ((((((triple3) -> rule1) ((((triple4) -> rule1)) -> rule3)) -> rule6)) -> rule1))]
("lion" "sees" "bald eagle" "-")
((((((triple3) -> (rule1 % int4)) ((((triple3) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int3
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int4
((((((triple3) -> (rule1 % int5)) ((((triple4) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int3
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int4
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int5
The bald eagle does not like the tiger.
True
8
proof
[(((((((((triple3) -> rule1) ((((triple3) -> rule1)) -> rule3)) -> rule6)) -> rule1)) -> rule2) OR ((((((((triple3) -> rule1) ((((triple4) -> rule1)) -> rule3)) -> rule6)) -> rule1)) -> rule2))]
("bald eagle" "likes" "tiger" "-")
((((((((triple3) -> (rule1 % int5)) ((((triple3) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle does not like the tiger.
("bald eagle" "likes" "tiger" "-")
int1
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int4
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int5
((((((((triple3) -> (rule1 % int6)) ((((triple4) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle does not like the tiger.
("bald eagle" "likes" "tiger" "-")
int1
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int4
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int5
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int6
The bald eagle likes the tiger.
False
8
inv-proof
[(((((((((triple3) -> rule1) ((((triple3) -> rule1)) -> rule3)) -> rule6)) -> rule1)) -> rule2) OR ((((((((triple3) -> rule1) ((((triple4) -> rule1)) -> rule3)) -> rule6)) -> rule1)) -> rule2))]
("bald eagle" "likes" "tiger" "+")
((((((((triple3) -> (rule1 % int5)) ((((triple3) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle does not like the tiger.
("bald eagle" "likes" "tiger" "-")
int1
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int4
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int5
((((((((triple3) -> (rule1 % int6)) ((((triple4) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle does not like the tiger.
("bald eagle" "likes" "tiger" "-")
int1
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int4
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int5
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int6
The tiger does not need the tiger.
Unknown
inv-rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "needs" "tiger" "-")
The bald eagle is round.
Unknown
rconc
[@1: The bald eagle is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bald eagle" "is" "round" "+")
The lion is not round.
Unknown
inv-rconc
[@1: The lion is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "is" "round" "-")
The cat likes the bald eagle.
Unknown
rconc
[@1: The cat likes the bald eagle.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "likes" "bald eagle" "+")
The bald eagle does not need the tiger.
Unknown
inv-rconc
[@1: The bald eagle needs the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bald eagle" "needs" "tiger" "-")
The cat needs the tiger.
Unknown
rconc
[@1: The cat needs the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "needs" "tiger" "+")
The bald eagle is not green.
Unknown
inv-random
[@0: The bald eagle is green.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "green" "-")
The tiger is green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
The cat does not see the lion.
Unknown
inv-random
[@0: The cat sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "lion" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The bald eagle is cold.[(triple1)] The bald eagle is young.[(triple2)] The bald eagle sees the tiger.[(triple3)] The cat sees the tiger.[(triple4)] The lion does not like the tiger.[(triple5)] The tiger does not see the cat.[(triple7)] The tiger is cold.[(triple6)] @1: The bald eagle sees the bald eagle.[(((triple3) -> rule1))] The cat sees the bald eagle.[(((triple4) -> rule1))] @2: The bald eagle sees the lion.[(((((triple3) -> rule1)) -> rule3) OR ((((triple4) -> rule1)) -> rule3))] @3: The lion sees the tiger.[(((((triple3) -> rule1) ((((triple3) -> rule1)) -> rule3)) -> rule6) OR ((((triple3) -> rule1) ((((triple4) -> rule1)) -> rule3)) -> rule6))] @4: The lion sees the bald eagle.[(((((((triple3) -> rule1) ((((triple3) -> rule1)) -> rule3)) -> rule6)) -> rule1) OR ((((((triple3) -> rule1) ((((triple4) -> rule1)) -> rule3)) -> rule6)) -> rule1))] @5: The bald eagle does not like the tiger.[(((((((((triple3) -> rule1) ((((triple3) -> rule1)) -> rule3)) -> rule6)) -> rule1)) -> rule2) OR ((((((((triple3) -> rule1) ((((triple4) -> rule1)) -> rule3)) -> rule6)) -> rule1)) -> rule2))]
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
triple1
The bald eagle is young.
("bald eagle" "is" "young" "+")
triple2
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
triple3
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple4
The lion does not like the tiger.
("lion" "likes" "tiger" "-")
triple5
The tiger does not see the cat.
("tiger" "sees" "cat" "-")
triple7
The tiger is cold.
("tiger" "is" "cold" "+")
triple6
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
((triple3) -> (rule1 % int1))
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
((triple4) -> (rule1 % int1))
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int1
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int2
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
((((triple3) -> (rule1 % int3)) ((((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int2
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int3
((((triple3) -> (rule1 % int4)) ((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int2
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int3
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int4
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
((((((triple3) -> (rule1 % int4)) ((((triple3) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int3
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int4
((((((triple3) -> (rule1 % int5)) ((((triple4) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int3
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int4
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int5
The bald eagle does not like the tiger.
("bald eagle" "likes" "tiger" "-")
((((((((triple3) -> (rule1 % int5)) ((((triple3) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle does not like the tiger.
("bald eagle" "likes" "tiger" "-")
int1
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int4
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int5
((((((((triple3) -> (rule1 % int6)) ((((triple4) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle does not like the tiger.
("bald eagle" "likes" "tiger" "-")
int1
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int4
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int5
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int6