The cow is red. The dog visits the mouse. The mouse chases the rabbit. The mouse sees the rabbit. The mouse visits the rabbit. The rabbit chases the dog. The rabbit is green. The rabbit sees the dog. The rabbit visits the cow. The rabbit visits the mouse. If something visits the dog then it sees the cow. If something sees the cow and it visits the cow then the cow visits the dog. If something chases the rabbit and the rabbit is green then the rabbit visits the dog.
The cow is red.
("cow" "is" "red" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If something visits the dog then it sees the cow.
((("something" "visits" "dog" "+")) -> ("something" "sees" "cow" "+"))
If something sees the cow and it visits the cow then the cow visits the dog.
((("something" "sees" "cow" "+") ("something" "visits" "cow" "+")) -> ("cow" "visits" "dog" "+"))
If something chases the rabbit and the rabbit is green then the rabbit visits the dog.
((("something" "chases" "rabbit" "+") ("rabbit" "is" "green" "+")) -> ("rabbit" "visits" "dog" "+"))
The mouse chases the rabbit.
True
1
proof
[(triple3)]
("mouse" "chases" "rabbit" "+")
triple3
The rabbit does not visit the mouse.
False
1
inv-proof
[(triple10)]
("rabbit" "visits" "mouse" "-")
triple10
The rabbit visits the dog.
True
3
proof
[(((triple3 triple7) -> rule3))]
("rabbit" "visits" "dog" "+")
((triple3 triple7) -> (rule3 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The rabbit does not visit the dog.
False
3
inv-proof
[(((triple3 triple7) -> rule3))]
("rabbit" "visits" "dog" "-")
((triple3 triple7) -> (rule3 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The rabbit sees the cow.
True
4
proof
[(((((triple3 triple7) -> rule3)) -> rule1))]
("rabbit" "sees" "cow" "+")
((((triple3 triple7) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int2
The rabbit does not see the cow.
False
4
inv-proof
[(((((triple3 triple7) -> rule3)) -> rule1))]
("rabbit" "sees" "cow" "-")
((((triple3 triple7) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int2
The mouse does not see the cow.
Unknown
inv-rconc
[@1: The mouse sees the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "sees" "cow" "-")
The dog sees the cow.
Unknown
rconc
[@1: The dog sees the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "sees" "cow" "+")
The cow does not see the dog.
Unknown
inv-random
[@0: The cow sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "dog" "-")
The dog sees the mouse.
Unknown
random
[@0: The dog sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "mouse" "+")
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The dog chases the mouse.
Unknown
random
[@0: The dog chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "mouse" "+")
@0: The cow is red.[(triple1)] The dog visits the mouse.[(triple2)] The mouse chases the rabbit.[(triple3)] The mouse sees the rabbit.[(triple4)] The mouse visits the rabbit.[(triple5)] The rabbit chases the dog.[(triple6)] The rabbit is green.[(triple7)] The rabbit sees the dog.[(triple8)] The rabbit visits the cow.[(triple9)] The rabbit visits the mouse.[(triple10)] @1: The rabbit visits the dog.[(((triple3 triple7) -> rule3))] @2: The rabbit sees the cow.[(((((triple3 triple7) -> rule3)) -> rule1))] @3: The cow visits the dog.[(((((((triple3 triple7) -> rule3)) -> rule1) triple9) -> rule2))] @4: The cow sees the cow.[(((((((((triple3 triple7) -> rule3)) -> rule1) triple9) -> rule2)) -> rule1))]
The cow is red.
("cow" "is" "red" "+")
triple1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple2
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple3
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple4
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple5
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple6
The rabbit is green.
("rabbit" "is" "green" "+")
triple7
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple8
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple9
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple10
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
((triple3 triple7) -> (rule3 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
((((triple3 triple7) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int2
The cow visits the dog.
("cow" "visits" "dog" "+")
((((((triple3 triple7) -> (rule3 % int3))) -> (rule1 % int2)) triple9) -> (rule2 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int2
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int3
The cow sees the cow.
("cow" "sees" "cow" "+")
((((((((triple3 triple7) -> (rule3 % int4))) -> (rule1 % int3)) triple9) -> (rule2 % int2))) -> (rule1 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
int2
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int3
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int4