The dog likes the squirrel. The squirrel needs the tiger. The tiger is big. If something needs the squirrel then the squirrel does not visit the dog. Big things are round. If something needs the squirrel and the squirrel is cold then it does not like the dog. If something visits the squirrel and the squirrel is cold then the squirrel likes the dog. If something is round and it visits the squirrel then the squirrel needs the dog. If something visits the dog then it is big. If something is cold and it does not need the squirrel then it does not like the squirrel. If something needs the tiger then it visits the dog.
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
If something needs the squirrel then the squirrel does not visit the dog.
((("something" "needs" "squirrel" "+")) -> ("squirrel" "visits" "dog" "-"))
Big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If something needs the squirrel and the squirrel is cold then it does not like the dog.
((("something" "needs" "squirrel" "+") ("squirrel" "is" "cold" "+")) -> ("something" "likes" "dog" "-"))
If something visits the squirrel and the squirrel is cold then the squirrel likes the dog.
((("something" "visits" "squirrel" "+") ("squirrel" "is" "cold" "+")) -> ("squirrel" "likes" "dog" "+"))
If something is round and it visits the squirrel then the squirrel needs the dog.
((("something" "is" "round" "+") ("something" "visits" "squirrel" "+")) -> ("squirrel" "needs" "dog" "+"))
If something visits the dog then it is big.
((("something" "visits" "dog" "+")) -> ("something" "is" "big" "+"))
If something is cold and it does not need the squirrel then it does not like the squirrel.
((("something" "is" "cold" "+") ("something" "needs" "squirrel" "~")) -> ("something" "likes" "squirrel" "-"))
If something needs the tiger then it visits the dog.
((("something" "needs" "tiger" "+")) -> ("something" "visits" "dog" "+"))
The squirrel needs the tiger.
True
1
proof
[(triple2)]
("squirrel" "needs" "tiger" "+")
triple2
The squirrel does not need the tiger.
False
1
inv-proof
[(triple2)]
("squirrel" "needs" "tiger" "-")
triple2
The tiger is round.
True
2
proof
[(((triple3) -> rule2))]
("tiger" "is" "round" "+")
((triple3) -> (rule2 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The squirrel does not visit the dog.
False
2
inv-proof
[(((triple2) -> rule8))]
("squirrel" "visits" "dog" "-")
((triple2) -> (rule8 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
The squirrel is big.
True
3
proof
[(((((triple2) -> rule8)) -> rule6))]
("squirrel" "is" "big" "+")
((((triple2) -> (rule8 % int2))) -> (rule6 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2
The squirrel is not big.
False
3
inv-proof
[(((((triple2) -> rule8)) -> rule6))]
("squirrel" "is" "big" "-")
((((triple2) -> (rule8 % int2))) -> (rule6 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2
The squirrel is round.
True
4
proof
[(((((((triple2) -> rule8)) -> rule6)) -> rule2))]
("squirrel" "is" "round" "+")
((((((triple2) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int3
The squirrel is not round.
False
4
inv-proof
[(((((((triple2) -> rule8)) -> rule6)) -> rule2))]
("squirrel" "is" "round" "-")
((((((triple2) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int3
The squirrel does not like the dog.
Unknown
inv-rconc
[@1: The squirrel likes the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "likes" "dog" "-")
The dog is round.
Unknown
rconc
[@3: The dog is round.[CWA. Example of deepest failure = (rule2 <- rule6 <- rule8 <- FAIL)]]
("dog" "is" "round" "+")
The dog does not visit the dog.
Unknown
inv-rconc
[@1: The dog visits the dog.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "visits" "dog" "-")
The tiger visits the dog.
Unknown
rconc
[@1: The tiger visits the dog.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "visits" "dog" "+")
The dog is not cold.
Unknown
inv-random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "-")
The tiger needs the dog.
Unknown
random
[@0: The tiger needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "dog" "+")
The squirrel does not visit the tiger.
Unknown
inv-random
[@0: The squirrel visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "tiger" "-")
The dog is young.
Unknown
random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "+")
@0: The dog likes the squirrel.[(triple1)] The squirrel needs the tiger.[(triple2)] The tiger is big.[(triple3)] @1: The squirrel visits the dog.[(((triple2) -> rule8))] The tiger is round.[(((triple3) -> rule2))] @2: The squirrel is big.[(((((triple2) -> rule8)) -> rule6))] @3: The squirrel is round.[(((((((triple2) -> rule8)) -> rule6)) -> rule2))]
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
triple1
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple2
The tiger is big.
("tiger" "is" "big" "+")
triple3
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
((triple2) -> (rule8 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
((triple3) -> (rule2 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
((((triple2) -> (rule8 % int2))) -> (rule6 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
((((((triple2) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int3