The cat is young. The dog visits the cat. The squirrel is big. The tiger visits the cat. If the tiger visits the cat then the tiger is young. If something visits the tiger then it is nice. If the dog visits the tiger then the dog likes the tiger. If something is big then it visits the tiger. If the squirrel likes the dog and the squirrel visits the cat then the cat is big. If something likes the dog and the dog is rough then the dog is young. If something likes the dog and the dog visits the squirrel then the dog is green. If something likes the dog and it likes the squirrel then the squirrel likes the dog.
The cat is young.
("cat" "is" "young" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If the tiger visits the cat then the tiger is young.
((("tiger" "visits" "cat" "+")) -> ("tiger" "is" "young" "+"))
If something visits the tiger then it is nice.
((("something" "visits" "tiger" "+")) -> ("something" "is" "nice" "+"))
If the dog visits the tiger then the dog likes the tiger.
((("dog" "visits" "tiger" "+")) -> ("dog" "likes" "tiger" "+"))
If something is big then it visits the tiger.
((("something" "is" "big" "+")) -> ("something" "visits" "tiger" "+"))
If the squirrel likes the dog and the squirrel visits the cat then the cat is big.
((("squirrel" "likes" "dog" "+") ("squirrel" "visits" "cat" "+")) -> ("cat" "is" "big" "+"))
If something likes the dog and the dog is rough then the dog is young.
((("something" "likes" "dog" "+") ("dog" "is" "rough" "+")) -> ("dog" "is" "young" "+"))
If something likes the dog and the dog visits the squirrel then the dog is green.
((("something" "likes" "dog" "+") ("dog" "visits" "squirrel" "+")) -> ("dog" "is" "green" "+"))
If something likes the dog and it likes the squirrel then the squirrel likes the dog.
((("something" "likes" "dog" "+") ("something" "likes" "squirrel" "+")) -> ("squirrel" "likes" "dog" "+"))
The cat is young.
True
1
proof
[(triple1)]
("cat" "is" "young" "+")
triple1
The squirrel is not big.
False
1
inv-proof
[(triple3)]
("squirrel" "is" "big" "-")
triple3
The squirrel visits the tiger.
True
2
proof
[(((triple3) -> rule4))]
("squirrel" "visits" "tiger" "+")
((triple3) -> (rule4 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel does not visit the tiger.
False
2
inv-proof
[(((triple3) -> rule4))]
("squirrel" "visits" "tiger" "-")
((triple3) -> (rule4 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel is nice.
True
3
proof
[(((((triple3) -> rule4)) -> rule2))]
("squirrel" "is" "nice" "+")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int2
The squirrel is not nice.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule2))]
("squirrel" "is" "nice" "-")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int2
The tiger does not visit the tiger.
Unknown
inv-rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "visits" "tiger" "-")
The tiger is nice.
Unknown
rconc
[@2: The tiger is nice.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("tiger" "is" "nice" "+")
The dog is not young.
Unknown
inv-rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "is" "young" "-")
The squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
The squirrel does not like the cat.
Unknown
inv-random
[@0: The squirrel likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "cat" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
@0: The cat is young.[(triple1)] The dog visits the cat.[(triple2)] The squirrel is big.[(triple3)] The tiger visits the cat.[(triple4)] @1: The squirrel visits the tiger.[(((triple3) -> rule4))] The tiger is young.[(((triple4) -> rule1))] @2: The squirrel is nice.[(((((triple3) -> rule4)) -> rule2))]
The cat is young.
("cat" "is" "young" "+")
triple1
The dog visits the cat.
("dog" "visits" "cat" "+")
triple2
The squirrel is big.
("squirrel" "is" "big" "+")
triple3
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple4
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
((triple3) -> (rule4 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
((triple4) -> (rule1 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int2