The cat is big. The cat is green. The cat is kind. The cat needs the tiger. The cat does not see the tiger. The cat visits the tiger. The dog is big. The dog is green. The dog visits the cat. The dog does not visit the tiger. The tiger is big. The tiger is not green. The tiger is round. The tiger does not need the cat. The tiger sees the dog. The tiger visits the dog. If something is big then it visits the dog. If something visits the cat and the cat is not round then it needs the cat. If something sees the tiger and the tiger needs the dog then the dog visits the cat. If something sees the cat and the cat visits the tiger then it is not kind. If something sees the dog and it does not need the cat then the cat is green. If the cat visits the dog and the tiger does not need the cat then the dog is kind.
The cat is big.
("cat" "is" "big" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The cat does not see the tiger.
("cat" "sees" "tiger" "-")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is green.
("dog" "is" "green" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
The dog does not visit the tiger.
("dog" "visits" "tiger" "-")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is not green.
("tiger" "is" "green" "-")
The tiger is round.
("tiger" "is" "round" "+")
The tiger does not need the cat.
("tiger" "needs" "cat" "-")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If something is big then it visits the dog.
((("something" "is" "big" "+")) -> ("something" "visits" "dog" "+"))
If something visits the cat and the cat is not round then it needs the cat.
((("something" "visits" "cat" "+") ("cat" "is" "round" "~")) -> ("something" "needs" "cat" "+"))
If something sees the tiger and the tiger needs the dog then the dog visits the cat.
((("something" "sees" "tiger" "+") ("tiger" "needs" "dog" "+")) -> ("dog" "visits" "cat" "+"))
If something sees the cat and the cat visits the tiger then it is not kind.
((("something" "sees" "cat" "+") ("cat" "visits" "tiger" "+")) -> ("something" "is" "kind" "-"))
If something sees the dog and it does not need the cat then the cat is green.
((("something" "sees" "dog" "+") ("something" "needs" "cat" "~")) -> ("cat" "is" "green" "+"))
If the cat visits the dog and the tiger does not need the cat then the dog is kind.
((("cat" "visits" "dog" "+") ("tiger" "needs" "cat" "~")) -> ("dog" "is" "kind" "+"))
The dog visits the cat.
True
1
proof
[(triple9)]
("dog" "visits" "cat" "+")
triple9
The cat does not visit the tiger.
False
1
inv-proof
[(triple6)]
("cat" "visits" "tiger" "-")
triple6
The dog visits the dog.
True
2
proof
[(((triple7) -> rule1))]
("dog" "visits" "dog" "+")
((triple7) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog does not visit the dog.
False
2
inv-proof
[(((triple7) -> rule1))]
("dog" "visits" "dog" "-")
((triple7) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is kind.
True
4
proof
[(((((triple1) -> rule1) triple14) -> rule6))]
("dog" "is" "kind" "+")
((((triple1) -> (rule1 % int2)) triple14) -> (rule6 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The dog is not kind.
False
4
inv-proof
[(((((triple1) -> rule1) triple14) -> rule6))]
("dog" "is" "kind" "-")
((((triple1) -> (rule1 % int2)) triple14) -> (rule6 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The dog does not need the cat.
Unknown
inv-rconc
[@1: The dog needs the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "needs" "cat" "-")
The cat needs the cat.
Unknown
rconc
[@1: The cat needs the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "needs" "cat" "+")
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The dog needs the tiger.
Unknown
random
[@0: The dog needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "tiger" "+")
The tiger is not red.
Unknown
inv-random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "-")
The dog sees the cat.
Unknown
random
[@0: The dog sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "cat" "+")
@0: The cat does not see the tiger.[(triple5)] The cat is big.[(triple1)] The cat is green.[(triple2 OR ((triple15 triple14) -> rule5))] The cat is kind.[(triple3)] The cat needs the tiger.[(triple4)] The cat visits the tiger.[(triple6)] The dog does not visit the tiger.[(triple10)] The dog is big.[(triple7)] The dog is green.[(triple8)] The dog visits the cat.[(triple9)] The tiger does not need the cat.[(triple14)] The tiger is big.[(triple11)] The tiger is not green.[(triple12)] The tiger is round.[(triple13)] The tiger sees the dog.[(triple15)] The tiger visits the dog.[(triple16 OR ((triple11) -> rule1))] @1: The cat visits the dog.[(((triple1) -> rule1))] The dog visits the dog.[(((triple7) -> rule1))] @2: The dog is kind.[(((((triple1) -> rule1) triple14) -> rule6))]
The cat does not see the tiger.
("cat" "sees" "tiger" "-")
triple5
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is green.
("cat" "is" "green" "+")
triple2
((triple15 triple14) -> (rule5 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
triple3
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple4
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple6
The dog does not visit the tiger.
("dog" "visits" "tiger" "-")
triple10
The dog is big.
("dog" "is" "big" "+")
triple7
The dog is green.
("dog" "is" "green" "+")
triple8
The dog visits the cat.
("dog" "visits" "cat" "+")
triple9
The tiger does not need the cat.
("tiger" "needs" "cat" "-")
triple14
The tiger is big.
("tiger" "is" "big" "+")
triple11
The tiger is not green.
("tiger" "is" "green" "-")
triple12
The tiger is round.
("tiger" "is" "round" "+")
triple13
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple15
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple16
((triple11) -> (rule1 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
((triple1) -> (rule1 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
((triple7) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
((((triple1) -> (rule1 % int2)) triple14) -> (rule6 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2