The cat is green. The cat sees the dog. The cat visits the rabbit. The dog eats the cat. The rabbit is blue. The squirrel is big. The squirrel is not round. Blue things are big. If something is big then it visits the dog. If something visits the dog then the dog sees the cat.
The cat is green.
("cat" "is" "green" "+")
The cat sees the dog.
("cat" "sees" "dog" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The dog eats the cat.
("dog" "eats" "cat" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is not round.
("squirrel" "is" "round" "-")
Blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something is big then it visits the dog.
((("something" "is" "big" "+")) -> ("something" "visits" "dog" "+"))
If something visits the dog then the dog sees the cat.
((("something" "visits" "dog" "+")) -> ("dog" "sees" "cat" "+"))
The squirrel is big.
True
1
proof
[(triple6)]
("squirrel" "is" "big" "+")
triple6
The squirrel is round.
False
1
inv-proof
[(triple7)]
("squirrel" "is" "round" "+")
triple7
The squirrel visits the dog.
True
2
proof
[(((triple6) -> rule2))]
("squirrel" "visits" "dog" "+")
((triple6) -> (rule2 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
The rabbit is not big.
False
2
inv-proof
[(((triple5) -> rule1))]
("rabbit" "is" "big" "-")
((triple5) -> (rule1 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The dog sees the cat.
True
3
proof
[(((((triple6) -> rule2)) -> rule3) OR ((((((triple5) -> rule1)) -> rule2)) -> rule3))]
("dog" "sees" "cat" "+")
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2
((((((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
The dog does not see the cat.
False
3
inv-proof
[(((((triple6) -> rule2)) -> rule3) OR ((((((triple5) -> rule1)) -> rule2)) -> rule3))]
("dog" "sees" "cat" "-")
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2
((((((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
The cat does not visit the dog.
Unknown
inv-rconc
[@2: The cat visits the dog.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("cat" "visits" "dog" "-")
The cat is big.
Unknown
rconc
[@1: The cat is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "big" "+")
The dog does not visit the dog.
Unknown
inv-rconc
[@2: The dog visits the dog.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("dog" "visits" "dog" "-")
The rabbit visits the squirrel.
Unknown
random
[@0: The rabbit visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "squirrel" "+")
The cat does not eat the rabbit.
Unknown
inv-random
[@0: The cat eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "rabbit" "-")
The cat eats the squirrel.
Unknown
random
[@0: The cat eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "squirrel" "+")
@0: The cat is green.[(triple1)] The cat sees the dog.[(triple2)] The cat visits the rabbit.[(triple3)] The dog eats the cat.[(triple4)] The rabbit is blue.[(triple5)] The squirrel is big.[(triple6)] The squirrel is not round.[(triple7)] @1: The rabbit is big.[(((triple5) -> rule1))] The squirrel visits the dog.[(((triple6) -> rule2))] @2: The dog sees the cat.[(((((triple6) -> rule2)) -> rule3) OR ((((((triple5) -> rule1)) -> rule2)) -> rule3))] The rabbit visits the dog.[(((((triple5) -> rule1)) -> rule2))]
The cat is green.
("cat" "is" "green" "+")
triple1
The cat sees the dog.
("cat" "sees" "dog" "+")
triple2
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple3
The dog eats the cat.
("dog" "eats" "cat" "+")
triple4
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple5
The squirrel is big.
("squirrel" "is" "big" "+")
triple6
The squirrel is not round.
("squirrel" "is" "round" "-")
triple7
The rabbit is big.
("rabbit" "is" "big" "+")
((triple5) -> (rule1 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
((triple6) -> (rule2 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2
((((((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2