The bald eagle does not need the mouse. The bald eagle sees the lion. The dog needs the lion. The dog needs the mouse. The lion chases the dog. The lion is nice. The mouse is big. If something chases the mouse and it sees the mouse then it is big. If something sees the dog then it is young. If something is young then it is red. If the lion chases the dog and the lion is nice then the dog is young. If something chases the dog then it sees the mouse. If something is red then it chases the mouse. If something needs the bald eagle then the bald eagle is not big. If the lion sees the dog and the dog does not need the lion then the lion sees the bald eagle. If something needs the lion then the lion sees the dog.
The bald eagle does not need the mouse.
("bald eagle" "needs" "mouse" "-")
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion is nice.
("lion" "is" "nice" "+")
The mouse is big.
("mouse" "is" "big" "+")
If something chases the mouse and it sees the mouse then it is big.
((("something" "chases" "mouse" "+") ("something" "sees" "mouse" "+")) -> ("something" "is" "big" "+"))
If something sees the dog then it is young.
((("something" "sees" "dog" "+")) -> ("something" "is" "young" "+"))
If something is young then it is red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If the lion chases the dog and the lion is nice then the dog is young.
((("lion" "chases" "dog" "+") ("lion" "is" "nice" "+")) -> ("dog" "is" "young" "+"))
If something chases the dog then it sees the mouse.
((("something" "chases" "dog" "+")) -> ("something" "sees" "mouse" "+"))
If something is red then it chases the mouse.
((("something" "is" "red" "+")) -> ("something" "chases" "mouse" "+"))
If something needs the bald eagle then the bald eagle is not big.
((("something" "needs" "bald eagle" "+")) -> ("bald eagle" "is" "big" "-"))
If the lion sees the dog and the dog does not need the lion then the lion sees the bald eagle.
((("lion" "sees" "dog" "+") ("dog" "needs" "lion" "~")) -> ("lion" "sees" "bald eagle" "+"))
If something needs the lion then the lion sees the dog.
((("something" "needs" "lion" "+")) -> ("lion" "sees" "dog" "+"))
The lion chases the dog.
True
1
proof
[(triple5)]
("lion" "chases" "dog" "+")
triple5
The bald eagle does not see the lion.
False
1
inv-proof
[(triple2)]
("bald eagle" "sees" "lion" "-")
triple2
The lion sees the mouse.
True
2
proof
[(((triple5) -> rule5))]
("lion" "sees" "mouse" "+")
((triple5) -> (rule5 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The dog is not young.
False
3
inv-proof
[(((triple5 triple6) -> rule4))]
("dog" "is" "young" "-")
((triple5 triple6) -> (rule4 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is red.
True
4
proof
[(((((triple5 triple6) -> rule4)) -> rule3))]
("dog" "is" "red" "+")
((((triple5 triple6) -> (rule4 % int2))) -> (rule3 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The lion is not young.
False
3
inv-proof
[(((((triple3) -> rule9)) -> rule2))]
("lion" "is" "young" "-")
((((triple3) -> (rule9 % int2))) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion sees the dog.
("lion" "sees" "dog" "+")
int2
The lion is red.
True
4
proof
[(((((((triple3) -> rule9)) -> rule2)) -> rule3))]
("lion" "is" "red" "+")
((((((triple3) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion sees the dog.
("lion" "sees" "dog" "+")
int3
The lion is not red.
False
4
inv-proof
[(((((((triple3) -> rule9)) -> rule2)) -> rule3))]
("lion" "is" "red" "-")
((((((triple3) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion sees the dog.
("lion" "sees" "dog" "+")
int3
The lion chases the mouse.
True
5
proof
[(((((((((triple3) -> rule9)) -> rule2)) -> rule3)) -> rule6))]
("lion" "chases" "mouse" "+")
((((((((triple3) -> (rule9 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion sees the dog.
("lion" "sees" "dog" "+")
int4
The lion does not chase the mouse.
False
5
inv-proof
[(((((((((triple3) -> rule9)) -> rule2)) -> rule3)) -> rule6))]
("lion" "chases" "mouse" "-")
((((((((triple3) -> (rule9 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion sees the dog.
("lion" "sees" "dog" "+")
int4
The lion is big.
True
8
proof
[(((((((((((triple3) -> rule9)) -> rule2)) -> rule3)) -> rule6) ((triple5) -> rule5)) -> rule1))]
("lion" "is" "big" "+")
((((((((((triple3) -> (rule9 % int6))) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule6 % int3)) ((triple5) -> (rule5 % int2))) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5
The lion sees the dog.
("lion" "sees" "dog" "+")
int6
The lion is not big.
False
8
inv-proof
[(((((((((((triple3) -> rule9)) -> rule2)) -> rule3)) -> rule6) ((triple5) -> rule5)) -> rule1))]
("lion" "is" "big" "-")
((((((((((triple3) -> (rule9 % int6))) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule6 % int3)) ((triple5) -> (rule5 % int2))) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5
The lion sees the dog.
("lion" "sees" "dog" "+")
int6
The lion does not see the bald eagle.
Unknown
inv-rconc
[@1: The lion sees the bald eagle.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "sees" "bald eagle" "-")
The bald eagle chases the mouse.
Unknown
rconc
[@3: The bald eagle chases the mouse.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule2 <- FAIL)]]
("bald eagle" "chases" "mouse" "+")
The mouse does not chase the mouse.
Unknown
inv-rconc
[@3: The mouse chases the mouse.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule2 <- FAIL)]]
("mouse" "chases" "mouse" "-")
The mouse is young.
Unknown
rconc
[@1: The mouse is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "young" "+")
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse is red.
Unknown
rconc
[@2: The mouse is red.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("mouse" "is" "red" "+")
The mouse is not rough.
Unknown
inv-random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "-")
The lion needs the bald eagle.
Unknown
random
[@0: The lion needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "bald eagle" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The dog is rough.
Unknown
random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "+")
The bald eagle does not need the dog.
Unknown
inv-random
[@0: The bald eagle needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "dog" "-")
The lion needs the dog.
Unknown
random
[@0: The lion needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "dog" "+")
@0: The bald eagle does not need the mouse.[(triple1)] The bald eagle sees the lion.[(triple2)] The dog needs the lion.[(triple3)] The dog needs the mouse.[(triple4)] The lion chases the dog.[(triple5)] The lion is nice.[(triple6)] The mouse is big.[(triple7)] @1: The dog is young.[(((triple5 triple6) -> rule4))] The lion sees the dog.[(((triple3) -> rule9))] The lion sees the mouse.[(((triple5) -> rule5))] @2: The dog is red.[(((((triple5 triple6) -> rule4)) -> rule3))] The lion is young.[(((((triple3) -> rule9)) -> rule2))] @3: The dog chases the mouse.[(((((((triple5 triple6) -> rule4)) -> rule3)) -> rule6))] The lion is red.[(((((((triple3) -> rule9)) -> rule2)) -> rule3))] @4: The lion chases the mouse.[(((((((((triple3) -> rule9)) -> rule2)) -> rule3)) -> rule6))] @5: The lion is big.[(((((((((((triple3) -> rule9)) -> rule2)) -> rule3)) -> rule6) ((triple5) -> rule5)) -> rule1))]
The bald eagle does not need the mouse.
("bald eagle" "needs" "mouse" "-")
triple1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
triple2
The dog needs the lion.
("dog" "needs" "lion" "+")
triple3
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple4
The lion chases the dog.
("lion" "chases" "dog" "+")
triple5
The lion is nice.
("lion" "is" "nice" "+")
triple6
The mouse is big.
("mouse" "is" "big" "+")
triple7
The dog is young.
("dog" "is" "young" "+")
((triple5 triple6) -> (rule4 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The lion sees the dog.
("lion" "sees" "dog" "+")
((triple3) -> (rule9 % int1))
The lion sees the dog.
("lion" "sees" "dog" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
((triple5) -> (rule5 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The dog is red.
("dog" "is" "red" "+")
((((triple5 triple6) -> (rule4 % int2))) -> (rule3 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The lion is young.
("lion" "is" "young" "+")
((((triple3) -> (rule9 % int2))) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion sees the dog.
("lion" "sees" "dog" "+")
int2
The dog chases the mouse.
("dog" "chases" "mouse" "+")
((((((triple5 triple6) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The lion is red.
("lion" "is" "red" "+")
((((((triple3) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion sees the dog.
("lion" "sees" "dog" "+")
int3
The lion chases the mouse.
("lion" "chases" "mouse" "+")
((((((((triple3) -> (rule9 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion sees the dog.
("lion" "sees" "dog" "+")
int4
The lion is big.
("lion" "is" "big" "+")
((((((((((triple3) -> (rule9 % int6))) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule6 % int3)) ((triple5) -> (rule5 % int2))) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5
The lion sees the dog.
("lion" "sees" "dog" "+")
int6