The cat chases the dog. The cat is not kind. The dog eats the cat. If the cat chases the dog then the dog is round. If the dog does not visit the cat then the dog eats the cat. If something eats the dog and the dog visits the cat then it does not chase the cat. If something chases the cat then the cat visits the dog. If the dog visits the cat then the cat chases the dog. All round things are young.
The cat chases the dog.
("cat" "chases" "dog" "+")
The cat is not kind.
("cat" "is" "kind" "-")
The dog eats the cat.
("dog" "eats" "cat" "+")
If the cat chases the dog then the dog is round.
((("cat" "chases" "dog" "+")) -> ("dog" "is" "round" "+"))
If the dog does not visit the cat then the dog eats the cat.
((("dog" "visits" "cat" "~")) -> ("dog" "eats" "cat" "+"))
If something eats the dog and the dog visits the cat then it does not chase the cat.
((("something" "eats" "dog" "+") ("dog" "visits" "cat" "+")) -> ("something" "chases" "cat" "-"))
If something chases the cat then the cat visits the dog.
((("something" "chases" "cat" "+")) -> ("cat" "visits" "dog" "+"))
If the dog visits the cat then the cat chases the dog.
((("dog" "visits" "cat" "+")) -> ("cat" "chases" "dog" "+"))
All round things are young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
The dog eats the cat.
True
1
proof
[(triple3)]
("dog" "eats" "cat" "+")
triple3
The cat does not chase the dog.
False
1
inv-proof
[(triple1)]
("cat" "chases" "dog" "-")
triple1
The dog is round.
True
2
proof
[(((triple1) -> rule1))]
("dog" "is" "round" "+")
((triple1) -> (rule1 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is not round.
False
2
inv-proof
[(((triple1) -> rule1))]
("dog" "is" "round" "-")
((triple1) -> (rule1 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is young.
True
3
proof
[(((((triple1) -> rule1)) -> rule6))]
("dog" "is" "young" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog is not young.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule6))]
("dog" "is" "young" "-")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The cat is not young.
Unknown
inv-rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "is" "young" "-")
The cat visits the dog.
Unknown
rconc
[@1: The cat visits the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "visits" "dog" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The cat eats the dog.
Unknown
random
[@0: The cat eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "dog" "+")
The cat is not cold.
Unknown
inv-random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat chases the dog.[(triple1)] The cat is not kind.[(triple2)] The dog eats the cat.[(triple3)] @1: The dog is round.[(((triple1) -> rule1))] @2: The dog is young.[(((((triple1) -> rule1)) -> rule6))]
The cat chases the dog.
("cat" "chases" "dog" "+")
triple1
The cat is not kind.
("cat" "is" "kind" "-")
triple2
The dog eats the cat.
("dog" "eats" "cat" "+")
triple3
The dog is round.
("dog" "is" "round" "+")
((triple1) -> (rule1 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is young.
("dog" "is" "young" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2