The cat sees the rabbit. The cat visits the mouse. The dog chases the mouse. The dog is blue. The dog is rough. The dog is round. The dog is young. The dog visits the cat. The mouse chases the rabbit. The mouse is rough. The mouse sees the rabbit. The mouse visits the dog. The mouse visits the rabbit. The rabbit chases the dog. The rabbit visits the cat. The rabbit visits the mouse. If something is blue and it sees the cat then it chases the dog. If the cat sees the rabbit and the cat is green then the cat is young. If the rabbit chases the dog and the rabbit visits the dog then the dog sees the cat. If the dog is green then the dog sees the cat. If the dog chases the mouse then the dog visits the rabbit. If something is young then it visits the cat. All round things are young. If the rabbit chases the mouse and the mouse is green then the rabbit sees the cat.
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is round.
("dog" "is" "round" "+")
The dog is young.
("dog" "is" "young" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If something is blue and it sees the cat then it chases the dog.
((("something" "is" "blue" "+") ("something" "sees" "cat" "+")) -> ("something" "chases" "dog" "+"))
If the cat sees the rabbit and the cat is green then the cat is young.
((("cat" "sees" "rabbit" "+") ("cat" "is" "green" "+")) -> ("cat" "is" "young" "+"))
If the rabbit chases the dog and the rabbit visits the dog then the dog sees the cat.
((("rabbit" "chases" "dog" "+") ("rabbit" "visits" "dog" "+")) -> ("dog" "sees" "cat" "+"))
If the dog is green then the dog sees the cat.
((("dog" "is" "green" "+")) -> ("dog" "sees" "cat" "+"))
If the dog chases the mouse then the dog visits the rabbit.
((("dog" "chases" "mouse" "+")) -> ("dog" "visits" "rabbit" "+"))
If something is young then it visits the cat.
((("something" "is" "young" "+")) -> ("something" "visits" "cat" "+"))
All round things are young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
If the rabbit chases the mouse and the mouse is green then the rabbit sees the cat.
((("rabbit" "chases" "mouse" "+") ("mouse" "is" "green" "+")) -> ("rabbit" "sees" "cat" "+"))
The dog visits the cat.
True
1
proof
[(triple8 OR ((triple7) -> rule6) OR ((((triple6) -> rule7)) -> rule6))]
("dog" "visits" "cat" "+")
triple8
((triple7) -> (rule6 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
((((triple6) -> (rule7 % int2))) -> (rule6 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The mouse is not rough.
False
1
inv-proof
[(triple10)]
("mouse" "is" "rough" "-")
triple10
The rabbit does not see the cat.
Unknown
inv-rconc
[@1: The rabbit sees the cat.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "sees" "cat" "-")
The dog sees the mouse.
Unknown
random
[@0: The dog sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "mouse" "+")
@0: The cat sees the rabbit.[(triple1)] The cat visits the mouse.[(triple2)] The dog chases the mouse.[(triple3)] The dog is blue.[(triple4)] The dog is rough.[(triple5)] The dog is round.[(triple6)] The dog is young.[(triple7 OR ((triple6) -> rule7))] The dog visits the cat.[(triple8 OR ((triple7) -> rule6) OR ((((triple6) -> rule7)) -> rule6))] The mouse chases the rabbit.[(triple9)] The mouse is rough.[(triple10)] The mouse sees the rabbit.[(triple11)] The mouse visits the dog.[(triple12)] The mouse visits the rabbit.[(triple13)] The rabbit chases the dog.[(triple14)] The rabbit visits the cat.[(triple15)] The rabbit visits the mouse.[(triple16)] @1: The dog visits the rabbit.[(((triple3) -> rule5))]
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple2
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple3
The dog is blue.
("dog" "is" "blue" "+")
triple4
The dog is rough.
("dog" "is" "rough" "+")
triple5
The dog is round.
("dog" "is" "round" "+")
triple6
The dog is young.
("dog" "is" "young" "+")
triple7
((triple6) -> (rule7 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
triple8
((triple7) -> (rule6 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
((((triple6) -> (rule7 % int2))) -> (rule6 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple9
The mouse is rough.
("mouse" "is" "rough" "+")
triple10
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple11
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple12
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple13
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple14
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple15
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple16
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
((triple3) -> (rule5 % int1))
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int1