The bald eagle does not visit the dog. The dog visits the lion. The lion is kind. If something sees the dog then the dog sees the lion. If something is rough then it needs the bald eagle. If something is rough then it sees the lion. If something sees the lion then it needs the dog. If something visits the lion then it sees the dog. If something is big then it does not see the bald eagle.
The bald eagle does not visit the dog.
("bald eagle" "visits" "dog" "-")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion is kind.
("lion" "is" "kind" "+")
If something sees the dog then the dog sees the lion.
((("something" "sees" "dog" "+")) -> ("dog" "sees" "lion" "+"))
If something is rough then it needs the bald eagle.
((("something" "is" "rough" "+")) -> ("something" "needs" "bald eagle" "+"))
If something is rough then it sees the lion.
((("something" "is" "rough" "+")) -> ("something" "sees" "lion" "+"))
If something sees the lion then it needs the dog.
((("something" "sees" "lion" "+")) -> ("something" "needs" "dog" "+"))
If something visits the lion then it sees the dog.
((("something" "visits" "lion" "+")) -> ("something" "sees" "dog" "+"))
If something is big then it does not see the bald eagle.
((("something" "is" "big" "+")) -> ("something" "sees" "bald eagle" "-"))
The dog visits the lion.
True
1
proof
[(triple2)]
("dog" "visits" "lion" "+")
triple2
The bald eagle visits the dog.
False
1
inv-proof
[(triple1)]
("bald eagle" "visits" "dog" "+")
triple1
The dog sees the dog.
True
2
proof
[(((triple2) -> rule5))]
("dog" "sees" "dog" "+")
((triple2) -> (rule5 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog does not see the dog.
False
2
inv-proof
[(((triple2) -> rule5))]
("dog" "sees" "dog" "-")
((triple2) -> (rule5 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog sees the lion.
True
3
proof
[(((((triple2) -> rule5)) -> rule1))]
("dog" "sees" "lion" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The dog sees the lion.
("dog" "sees" "lion" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog does not see the lion.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule1))]
("dog" "sees" "lion" "-")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The dog sees the lion.
("dog" "sees" "lion" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog needs the dog.
True
4
proof
[(((((((triple2) -> rule5)) -> rule1)) -> rule4))]
("dog" "needs" "dog" "+")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog sees the lion.
("dog" "sees" "lion" "+")
int2
The dog sees the dog.
("dog" "sees" "dog" "+")
int3
The dog does not need the dog.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule1)) -> rule4))]
("dog" "needs" "dog" "-")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog sees the lion.
("dog" "sees" "lion" "+")
int2
The dog sees the dog.
("dog" "sees" "dog" "+")
int3
The dog does not need the bald eagle.
Unknown
inv-rconc
[@1: The dog needs the bald eagle.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "needs" "bald eagle" "-")
The lion sees the lion.
Unknown
rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "sees" "lion" "+")
The bald eagle does not see the lion.
Unknown
inv-rconc
[@1: The bald eagle sees the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bald eagle" "sees" "lion" "-")
The lion needs the bald eagle.
Unknown
rconc
[@1: The lion needs the bald eagle.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "needs" "bald eagle" "+")
The lion does not visit the dog.
Unknown
inv-random
[@0: The lion visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "dog" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
The lion does not see the bald eagle.
Unknown
inv-random
[@0: The lion sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "bald eagle" "-")
The bald eagle is big.
Unknown
random
[@0: The bald eagle is big.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "big" "+")
@0: The bald eagle does not visit the dog.[(triple1)] The dog visits the lion.[(triple2)] The lion is kind.[(triple3)] @1: The dog sees the dog.[(((triple2) -> rule5))] @2: The dog sees the lion.[(((((triple2) -> rule5)) -> rule1))] @3: The dog needs the dog.[(((((((triple2) -> rule5)) -> rule1)) -> rule4))]
The bald eagle does not visit the dog.
("bald eagle" "visits" "dog" "-")
triple1
The dog visits the lion.
("dog" "visits" "lion" "+")
triple2
The lion is kind.
("lion" "is" "kind" "+")
triple3
The dog sees the dog.
("dog" "sees" "dog" "+")
((triple2) -> (rule5 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog sees the lion.
("dog" "sees" "lion" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The dog sees the lion.
("dog" "sees" "lion" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog sees the lion.
("dog" "sees" "lion" "+")
int2
The dog sees the dog.
("dog" "sees" "dog" "+")
int3