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