The cow is young. The cow needs the lion. The cow sees the dog. The dog is big. The dog is cold. The dog is kind. The dog is not young. The dog needs the lion. The dog does not see the lion. The lion is kind. The lion is not young. The lion sees the cow. If someone needs the lion then the lion visits the dog. If the cow does not see the dog then the cow is not young. If someone is red then they are not kind. If someone visits the dog then they visit the cow. If the lion is not kind and the lion does not need the dog then the dog does not visit the cow. If someone visits the cow then the cow does not need the dog.
The cow is young.
("cow" "is" "young" "+")
The cow needs the lion.
("cow" "needs" "lion" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is not young.
("dog" "is" "young" "-")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog does not see the lion.
("dog" "sees" "lion" "-")
The lion is kind.
("lion" "is" "kind" "+")
The lion is not young.
("lion" "is" "young" "-")
The lion sees the cow.
("lion" "sees" "cow" "+")
If someone needs the lion then the lion visits the dog.
((("someone" "needs" "lion" "+")) -> ("lion" "visits" "dog" "+"))
If the cow does not see the dog then the cow is not young.
((("cow" "sees" "dog" "~")) -> ("cow" "is" "young" "-"))
If someone is red then they are not kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "-"))
If someone visits the dog then they visit the cow.
((("someone" "visits" "dog" "+")) -> ("someone" "visits" "cow" "+"))
If the lion is not kind and the lion does not need the dog then the dog does not visit the cow.
((("lion" "is" "kind" "~") ("lion" "needs" "dog" "~")) -> ("dog" "visits" "cow" "-"))
If someone visits the cow then the cow does not need the dog.
((("someone" "visits" "cow" "+")) -> ("cow" "needs" "dog" "-"))
The dog is not young.
True
1
proof
[(triple7)]
("dog" "is" "young" "-")
triple7
The dog sees the lion.
False
1
inv-proof
[(triple9)]
("dog" "sees" "lion" "+")
triple9
The lion visits the dog.
True
2
proof
[(((triple2) -> rule1) OR ((triple8) -> rule1))]
("lion" "visits" "dog" "+")
((triple2) -> (rule1 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
((triple8) -> (rule1 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The lion does not visit the dog.
False
2
inv-proof
[(((triple2) -> rule1) OR ((triple8) -> rule1))]
("lion" "visits" "dog" "-")
((triple2) -> (rule1 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
((triple8) -> (rule1 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The lion visits the cow.
True
3
proof
[(((((triple2) -> rule1)) -> rule4) OR ((((triple8) -> rule1)) -> rule4))]
("lion" "visits" "cow" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The lion visits the cow.
("lion" "visits" "cow" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
((((triple8) -> (rule1 % int2))) -> (rule4 % int1))
The lion visits the cow.
("lion" "visits" "cow" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The lion does not visit the cow.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule4) OR ((((triple8) -> rule1)) -> rule4))]
("lion" "visits" "cow" "-")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The lion visits the cow.
("lion" "visits" "cow" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
((((triple8) -> (rule1 % int2))) -> (rule4 % int1))
The lion visits the cow.
("lion" "visits" "cow" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The cow does not need the dog.
True
4
proof
[(((((((triple2) -> rule1)) -> rule4)) -> rule6) OR ((((((triple8) -> rule1)) -> rule4)) -> rule6))]
("cow" "needs" "dog" "-")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow does not need the dog.
("cow" "needs" "dog" "-")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The lion visits the dog.
("lion" "visits" "dog" "+")
int3
((((((triple8) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow does not need the dog.
("cow" "needs" "dog" "-")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The lion visits the dog.
("lion" "visits" "dog" "+")
int3
The cow needs the dog.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule4)) -> rule6) OR ((((((triple8) -> rule1)) -> rule4)) -> rule6))]
("cow" "needs" "dog" "+")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow does not need the dog.
("cow" "needs" "dog" "-")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The lion visits the dog.
("lion" "visits" "dog" "+")
int3
((((((triple8) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow does not need the dog.
("cow" "needs" "dog" "-")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The lion visits the dog.
("lion" "visits" "dog" "+")
int3
The cow does not visit the cow.
Unknown
inv-rconc
[@1: The cow visits the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "visits" "cow" "-")
The dog visits the cow.
Unknown
rconc
[@1: The dog visits the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "visits" "cow" "+")
The lion does not need the cow.
Unknown
inv-random
[@0: The lion needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "cow" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
The lion is not cold.
Unknown
inv-random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "-")
The dog visits the lion.
Unknown
random
[@0: The dog visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "lion" "+")
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
The cow visits the dog.
Unknown
random
[@0: The cow visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "dog" "+")
@0: The cow is young.[(triple1)] The cow needs the lion.[(triple2)] The cow sees the dog.[(triple3)] The dog does not see the lion.[(triple9)] The dog is big.[(triple4)] The dog is cold.[(triple5)] The dog is kind.[(triple6)] The dog is not young.[(triple7)] The dog needs the lion.[(triple8)] The lion is kind.[(triple10)] The lion is not young.[(triple11)] The lion sees the cow.[(triple12)] @1: The lion visits the dog.[(((triple2) -> rule1) OR ((triple8) -> rule1))] @2: The lion visits the cow.[(((((triple2) -> rule1)) -> rule4) OR ((((triple8) -> rule1)) -> rule4))] @3: The cow does not need the dog.[(((((((triple2) -> rule1)) -> rule4)) -> rule6) OR ((((((triple8) -> rule1)) -> rule4)) -> rule6))]
The cow is young.
("cow" "is" "young" "+")
triple1
The cow needs the lion.
("cow" "needs" "lion" "+")
triple2
The cow sees the dog.
("cow" "sees" "dog" "+")
triple3
The dog does not see the lion.
("dog" "sees" "lion" "-")
triple9
The dog is big.
("dog" "is" "big" "+")
triple4
The dog is cold.
("dog" "is" "cold" "+")
triple5
The dog is kind.
("dog" "is" "kind" "+")
triple6
The dog is not young.
("dog" "is" "young" "-")
triple7
The dog needs the lion.
("dog" "needs" "lion" "+")
triple8
The lion is kind.
("lion" "is" "kind" "+")
triple10
The lion is not young.
("lion" "is" "young" "-")
triple11
The lion sees the cow.
("lion" "sees" "cow" "+")
triple12
The lion visits the dog.
("lion" "visits" "dog" "+")
((triple2) -> (rule1 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
((triple8) -> (rule1 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The lion visits the cow.
("lion" "visits" "cow" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
((((triple8) -> (rule1 % int2))) -> (rule4 % int1))
The lion visits the cow.
("lion" "visits" "cow" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The cow does not need the dog.
("cow" "needs" "dog" "-")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow does not need the dog.
("cow" "needs" "dog" "-")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The lion visits the dog.
("lion" "visits" "dog" "+")
int3
((((((triple8) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow does not need the dog.
("cow" "needs" "dog" "-")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The lion visits the dog.
("lion" "visits" "dog" "+")
int3