The cow does not like the lion. The dog visits the cow. The lion visits the dog. The squirrel is kind. If someone is cold and they do not like the lion then they like the dog. If someone is kind and not cold then they visit the dog. If someone visits the lion then they do not see the cow. If someone is kind and they do not see the lion then the lion does not see the squirrel. All kind people are round. If someone is round then they visit the lion. If someone likes the cow and they do not like the lion then they visit the lion. If the cow sees the dog then the cow likes the dog.
The cow does not like the lion.
("cow" "likes" "lion" "-")
The dog visits the cow.
("dog" "visits" "cow" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
If someone is cold and they do not like the lion then they like the dog.
((("someone" "is" "cold" "+") ("someone" "likes" "lion" "~")) -> ("someone" "likes" "dog" "+"))
If someone is kind and not cold then they visit the dog.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "~")) -> ("someone" "visits" "dog" "+"))
If someone visits the lion then they do not see the cow.
((("someone" "visits" "lion" "+")) -> ("someone" "sees" "cow" "-"))
If someone is kind and they do not see the lion then the lion does not see the squirrel.
((("someone" "is" "kind" "+") ("someone" "sees" "lion" "~")) -> ("lion" "sees" "squirrel" "-"))
All kind people are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
If someone is round then they visit the lion.
((("someone" "is" "round" "+")) -> ("someone" "visits" "lion" "+"))
If someone likes the cow and they do not like the lion then they visit the lion.
((("someone" "likes" "cow" "+") ("someone" "likes" "lion" "~")) -> ("someone" "visits" "lion" "+"))
If the cow sees the dog then the cow likes the dog.
((("cow" "sees" "dog" "+")) -> ("cow" "likes" "dog" "+"))
The cow does not like the lion.
True
1
proof
[(triple1)]
("cow" "likes" "lion" "-")
triple1
The cow likes the lion.
False
1
inv-proof
[(triple1)]
("cow" "likes" "lion" "+")
triple1
The squirrel is round.
True
2
proof
[(((triple4) -> rule5))]
("squirrel" "is" "round" "+")
((triple4) -> (rule5 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel is not round.
False
2
inv-proof
[(((triple4) -> rule5))]
("squirrel" "is" "round" "-")
((triple4) -> (rule5 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel visits the lion.
True
3
proof
[(((((triple4) -> rule5)) -> rule6))]
("squirrel" "visits" "lion" "+")
((((triple4) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The squirrel does not visit the lion.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule6))]
("squirrel" "visits" "lion" "-")
((((triple4) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The squirrel does not see the cow.
True
4
proof
[(((((((triple4) -> rule5)) -> rule6)) -> rule3))]
("squirrel" "sees" "cow" "-")
((((((triple4) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel does not see the cow.
("squirrel" "sees" "cow" "-")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The squirrel sees the cow.
False
4
inv-proof
[(((((((triple4) -> rule5)) -> rule6)) -> rule3))]
("squirrel" "sees" "cow" "+")
((((((triple4) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel does not see the cow.
("squirrel" "sees" "cow" "-")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The cow is not round.
Unknown
inv-rconc
[@1: The cow is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "is" "round" "-")
The lion visits the lion.
Unknown
rconc
[@2: The lion visits the lion.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("lion" "visits" "lion" "+")
The dog is not round.
Unknown
inv-rconc
[@1: The dog is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "round" "-")
The dog likes the dog.
Unknown
rconc
[@1: The dog likes the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "likes" "dog" "+")
The lion does not visit the cow.
Unknown
inv-random
[@0: The lion visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "cow" "-")
The squirrel is red.
Unknown
random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "+")
The squirrel does not like the cow.
Unknown
inv-random
[@0: The squirrel likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "cow" "-")
The squirrel likes the lion.
Unknown
random
[@0: The squirrel likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "lion" "+")
@0: The cow does not like the lion.[(triple1)] The dog visits the cow.[(triple2)] The lion visits the dog.[(triple3)] The squirrel is kind.[(triple4)] @1: The squirrel is round.[(((triple4) -> rule5))] @2: The squirrel visits the lion.[(((((triple4) -> rule5)) -> rule6))] @3: The squirrel does not see the cow.[(((((((triple4) -> rule5)) -> rule6)) -> rule3))]
The cow does not like the lion.
("cow" "likes" "lion" "-")
triple1
The dog visits the cow.
("dog" "visits" "cow" "+")
triple2
The lion visits the dog.
("lion" "visits" "dog" "+")
triple3
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple4
The squirrel is round.
("squirrel" "is" "round" "+")
((triple4) -> (rule5 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
((((triple4) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The squirrel does not see the cow.
("squirrel" "sees" "cow" "-")
((((((triple4) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel does not see the cow.
("squirrel" "sees" "cow" "-")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3