The cat is rough. The cat is round. The cat needs the dog. The cat sees the dog. The dog chases the cat. The dog is green. The dog is rough. The dog is round. The dog needs the cat. The dog sees the cat. If something is kind and it does not need the cat then the cat does not chase the dog. If something sees the dog and it is not green then the dog sees the cat. If the dog is big and the dog needs the cat then the dog does not see the cat. If something is kind and big then it is not rough. If something is rough and it chases the cat then it chases the dog. If the dog needs the cat then the dog is round.
The cat is rough.
("cat" "is" "rough" "+")
The cat is round.
("cat" "is" "round" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The cat sees the dog.
("cat" "sees" "dog" "+")
The dog chases the cat.
("dog" "chases" "cat" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is round.
("dog" "is" "round" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
If something is kind and it does not need the cat then the cat does not chase the dog.
((("something" "is" "kind" "+") ("something" "needs" "cat" "~")) -> ("cat" "chases" "dog" "-"))
If something sees the dog and it is not green then the dog sees the cat.
((("something" "sees" "dog" "+") ("something" "is" "green" "~")) -> ("dog" "sees" "cat" "+"))
If the dog is big and the dog needs the cat then the dog does not see the cat.
((("dog" "is" "big" "+") ("dog" "needs" "cat" "+")) -> ("dog" "sees" "cat" "-"))
If something is kind and big then it is not rough.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "-"))
If something is rough and it chases the cat then it chases the dog.
((("something" "is" "rough" "+") ("something" "chases" "cat" "+")) -> ("something" "chases" "dog" "+"))
If the dog needs the cat then the dog is round.
((("dog" "needs" "cat" "+")) -> ("dog" "is" "round" "+"))
The dog is round.
True
1
proof
[(triple8 OR ((triple9) -> rule6))]
("dog" "is" "round" "+")
triple8
((triple9) -> (rule6 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The cat is not round.
False
1
inv-proof
[(triple2)]
("cat" "is" "round" "-")
triple2
The cat does not chase the dog.
Unknown
inv-rconc
[@1: The cat chases the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "chases" "dog" "-")
The dog is kind.
Unknown
random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "+")
@0: The cat is rough.[(triple1)] The cat is round.[(triple2)] The cat needs the dog.[(triple3)] The cat sees the dog.[(triple4)] The dog chases the cat.[(triple5)] The dog is green.[(triple6)] The dog is rough.[(triple7)] The dog is round.[(triple8 OR ((triple9) -> rule6))] The dog needs the cat.[(triple9)] The dog sees the cat.[(triple10)] @1: The dog chases the dog.[(((triple7 triple5) -> rule5))]
The cat is rough.
("cat" "is" "rough" "+")
triple1
The cat is round.
("cat" "is" "round" "+")
triple2
The cat needs the dog.
("cat" "needs" "dog" "+")
triple3
The cat sees the dog.
("cat" "sees" "dog" "+")
triple4
The dog chases the cat.
("dog" "chases" "cat" "+")
triple5
The dog is green.
("dog" "is" "green" "+")
triple6
The dog is rough.
("dog" "is" "rough" "+")
triple7
The dog is round.
("dog" "is" "round" "+")
triple8
((triple9) -> (rule6 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog needs the cat.
("dog" "needs" "cat" "+")
triple9
The dog sees the cat.
("dog" "sees" "cat" "+")
triple10
The dog chases the dog.
("dog" "chases" "dog" "+")
((triple7 triple5) -> (rule5 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1