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