The cat is nice. The cat needs the squirrel. The cat sees the dog. The dog is nice. The dog is round. The dog is not young. The dog needs the cat. The dog needs the squirrel. The dog visits the cat. The dog visits the squirrel. The squirrel does not need the cat. The squirrel sees the dog. If someone is green then they visit the cat. If someone is young then they visit the cat. If someone needs the dog then the dog sees the squirrel. If someone visits the cat then they see the squirrel. If someone is round then they see the squirrel. If someone is nice and they do not need the squirrel then they see the dog. If someone is nice and they see the squirrel then they see the dog. If the dog sees the cat then the dog does not visit the squirrel.
The cat is nice.
("cat" "is" "nice" "+")
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The cat sees the dog.
("cat" "sees" "dog" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is round.
("dog" "is" "round" "+")
The dog is not young.
("dog" "is" "young" "-")
The dog needs the cat.
("dog" "needs" "cat" "+")
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
The squirrel does not need the cat.
("squirrel" "needs" "cat" "-")
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
If someone is green then they visit the cat.
((("someone" "is" "green" "+")) -> ("someone" "visits" "cat" "+"))
If someone is young then they visit the cat.
((("someone" "is" "young" "+")) -> ("someone" "visits" "cat" "+"))
If someone needs the dog then the dog sees the squirrel.
((("someone" "needs" "dog" "+")) -> ("dog" "sees" "squirrel" "+"))
If someone visits the cat then they see the squirrel.
((("someone" "visits" "cat" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone is round then they see the squirrel.
((("someone" "is" "round" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone is nice and they do not need the squirrel then they see the dog.
((("someone" "is" "nice" "+") ("someone" "needs" "squirrel" "~")) -> ("someone" "sees" "dog" "+"))
If someone is nice and they see the squirrel then they see the dog.
((("someone" "is" "nice" "+") ("someone" "sees" "squirrel" "+")) -> ("someone" "sees" "dog" "+"))
If the dog sees the cat then the dog does not visit the squirrel.
((("dog" "sees" "cat" "+")) -> ("dog" "visits" "squirrel" "-"))
The dog visits the cat.
True
1
proof
[(triple9)]
("dog" "visits" "cat" "+")
triple9
The cat is not nice.
False
1
inv-proof
[(triple1)]
("cat" "is" "nice" "-")
triple1
The dog sees the squirrel.
True
2
proof
[(((triple5) -> rule5) OR ((triple9) -> rule4))]
("dog" "sees" "squirrel" "+")
((triple5) -> (rule5 % int1))
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int1
((triple9) -> (rule4 % int1))
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int1
The dog does not see the squirrel.
False
2
inv-proof
[(((triple5) -> rule5) OR ((triple9) -> rule4))]
("dog" "sees" "squirrel" "-")
((triple5) -> (rule5 % int1))
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int1
((triple9) -> (rule4 % int1))
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int1
The dog sees the dog.
True
4
proof
[(((triple4 ((triple5) -> rule5)) -> rule7) OR ((triple4 ((triple9) -> rule4)) -> rule7))]
("dog" "sees" "dog" "+")
((triple4 ((triple5) -> (rule5 % int2))) -> (rule7 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int2
((triple4 ((triple9) -> (rule4 % int2))) -> (rule7 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int2
The dog does not see the dog.
False
4
inv-proof
[(((triple4 ((triple5) -> rule5)) -> rule7) OR ((triple4 ((triple9) -> rule4)) -> rule7))]
("dog" "sees" "dog" "-")
((triple4 ((triple5) -> (rule5 % int2))) -> (rule7 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int2
((triple4 ((triple9) -> (rule4 % int2))) -> (rule7 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int2
The squirrel does not visit the cat.
Unknown
inv-rconc
[@1: The squirrel visits the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "visits" "cat" "-")
The squirrel sees the squirrel.
Unknown
rconc
[@2: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("squirrel" "sees" "squirrel" "+")
The cat does not see the squirrel.
Unknown
inv-rconc
[@2: The cat sees the squirrel.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("cat" "sees" "squirrel" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
The squirrel is not young.
Unknown
inv-random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "-")
The cat visits the squirrel.
Unknown
random
[@0: The cat visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "squirrel" "+")
@0: The cat is nice.[(triple1)] The cat needs the squirrel.[(triple2)] The cat sees the dog.[(triple3)] The dog is nice.[(triple4)] The dog is not young.[(triple6)] The dog is round.[(triple5)] The dog needs the cat.[(triple7)] The dog needs the squirrel.[(triple8)] The dog visits the cat.[(triple9)] The dog visits the squirrel.[(triple10)] The squirrel does not need the cat.[(triple11)] The squirrel sees the dog.[(triple12)] @1: The dog sees the squirrel.[(((triple5) -> rule5) OR ((triple9) -> rule4))] @2: The dog sees the dog.[(((triple4 ((triple5) -> rule5)) -> rule7) OR ((triple4 ((triple9) -> rule4)) -> rule7))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple2
The cat sees the dog.
("cat" "sees" "dog" "+")
triple3
The dog is nice.
("dog" "is" "nice" "+")
triple4
The dog is not young.
("dog" "is" "young" "-")
triple6
The dog is round.
("dog" "is" "round" "+")
triple5
The dog needs the cat.
("dog" "needs" "cat" "+")
triple7
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
triple8
The dog visits the cat.
("dog" "visits" "cat" "+")
triple9
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
triple10
The squirrel does not need the cat.
("squirrel" "needs" "cat" "-")
triple11
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
triple12
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
((triple5) -> (rule5 % int1))
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int1
((triple9) -> (rule4 % int1))
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
((triple4 ((triple5) -> (rule5 % int2))) -> (rule7 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int2
((triple4 ((triple9) -> (rule4 % int2))) -> (rule7 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int2