The cat chases the mouse. The cat chases the rabbit. The cat is rough. The cow likes the rabbit. The mouse chases the cow. The mouse is round. The mouse likes the cat. The mouse likes the rabbit. The rabbit chases the cow. The rabbit eats the mouse. The rabbit likes the mouse. If something is rough and it likes the mouse then the mouse chases the rabbit. If the rabbit eats the cow and the rabbit is kind then the cow likes the cat. If something is red then it is young. If something is young then it likes the cow. If something chases the cat and it is round then it is red. If something is rough then it eats the cat. If something is round then it chases the cat. If something likes the cow then it chases the mouse. If something likes the rabbit and the rabbit is kind then it chases the cat.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
If something is rough and it likes the mouse then the mouse chases the rabbit.
((("something" "is" "rough" "+") ("something" "likes" "mouse" "+")) -> ("mouse" "chases" "rabbit" "+"))
If the rabbit eats the cow and the rabbit is kind then the cow likes the cat.
((("rabbit" "eats" "cow" "+") ("rabbit" "is" "kind" "+")) -> ("cow" "likes" "cat" "+"))
If something is red then it is young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If something is young then it likes the cow.
((("something" "is" "young" "+")) -> ("something" "likes" "cow" "+"))
If something chases the cat and it is round then it is red.
((("something" "chases" "cat" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If something is rough then it eats the cat.
((("something" "is" "rough" "+")) -> ("something" "eats" "cat" "+"))
If something is round then it chases the cat.
((("something" "is" "round" "+")) -> ("something" "chases" "cat" "+"))
If something likes the cow then it chases the mouse.
((("something" "likes" "cow" "+")) -> ("something" "chases" "mouse" "+"))
If something likes the rabbit and the rabbit is kind then it chases the cat.
((("something" "likes" "rabbit" "+") ("rabbit" "is" "kind" "+")) -> ("something" "chases" "cat" "+"))
The rabbit likes the mouse.
True
1
proof
[(triple11)]
("rabbit" "likes" "mouse" "+")
triple11
The mouse is not round.
False
1
inv-proof
[(triple6)]
("mouse" "is" "round" "-")
triple6
The cat eats the cat.
True
2
proof
[(((triple3) -> rule6))]
("cat" "eats" "cat" "+")
((triple3) -> (rule6 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat does not eat the cat.
False
2
inv-proof
[(((triple3) -> rule6))]
("cat" "eats" "cat" "-")
((triple3) -> (rule6 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The mouse is red.
True
4
proof
[(((((triple6) -> rule7) triple6) -> rule5))]
("mouse" "is" "red" "+")
((((triple6) -> (rule7 % int2)) triple6) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int2
The mouse is not red.
False
4
inv-proof
[(((((triple6) -> rule7) triple6) -> rule5))]
("mouse" "is" "red" "-")
((((triple6) -> (rule7 % int2)) triple6) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int2
The mouse is young.
True
5
proof
[(((((((triple6) -> rule7) triple6) -> rule5)) -> rule3))]
("mouse" "is" "young" "+")
((((((triple6) -> (rule7 % int3)) triple6) -> (rule5 % int2))) -> (rule3 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int3
The mouse is not young.
False
5
inv-proof
[(((((((triple6) -> rule7) triple6) -> rule5)) -> rule3))]
("mouse" "is" "young" "-")
((((((triple6) -> (rule7 % int3)) triple6) -> (rule5 % int2))) -> (rule3 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int3
The mouse likes the cow.
True
6
proof
[(((((((((triple6) -> rule7) triple6) -> rule5)) -> rule3)) -> rule4))]
("mouse" "likes" "cow" "+")
((((((((triple6) -> (rule7 % int4)) triple6) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int4
The mouse does not like the cow.
False
6
inv-proof
[(((((((((triple6) -> rule7) triple6) -> rule5)) -> rule3)) -> rule4))]
("mouse" "likes" "cow" "-")
((((((((triple6) -> (rule7 % int4)) triple6) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int4
The mouse chases the mouse.
True
7
proof
[(((((((((((triple6) -> rule7) triple6) -> rule5)) -> rule3)) -> rule4)) -> rule8))]
("mouse" "chases" "mouse" "+")
((((((((((triple6) -> (rule7 % int5)) triple6) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The mouse is red.
("mouse" "is" "red" "+")
int4
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int5
The mouse does not chase the mouse.
False
7
inv-proof
[(((((((((((triple6) -> rule7) triple6) -> rule5)) -> rule3)) -> rule4)) -> rule8))]
("mouse" "chases" "mouse" "-")
((((((((((triple6) -> (rule7 % int5)) triple6) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The mouse is red.
("mouse" "is" "red" "+")
int4
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int5
The mouse does not chase the rabbit.
Unknown
inv-rconc
[@1: The mouse chases the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "chases" "rabbit" "-")
The rabbit is red.
Unknown
rconc
[@1: The rabbit is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "red" "+")
The cow is not red.
Unknown
inv-rconc
[@1: The cow is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "is" "red" "-")
The cow likes the cat.
Unknown
rconc
[@1: The cow likes the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "likes" "cat" "+")
The rabbit does not eat the cat.
Unknown
inv-rconc
[@1: The rabbit eats the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "eats" "cat" "-")
The cow likes the cow.
Unknown
rconc
[@3: The cow likes the cow.[CWA. Example of deepest failure = (rule4 <- rule3 <- rule5 <- FAIL)]]
("cow" "likes" "cow" "+")
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The cow is not round.
Unknown
inv-random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "-")
The cat eats the mouse.
Unknown
random
[@0: The cat eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "mouse" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
@0: The cat chases the mouse.[(triple1)] The cat chases the rabbit.[(triple2)] The cat is rough.[(triple3)] The cow likes the rabbit.[(triple4)] The mouse chases the cow.[(triple5)] The mouse is round.[(triple6)] The mouse likes the cat.[(triple7)] The mouse likes the rabbit.[(triple8)] The rabbit chases the cow.[(triple9)] The rabbit eats the mouse.[(triple10)] The rabbit likes the mouse.[(triple11)] @1: The cat eats the cat.[(((triple3) -> rule6))] The mouse chases the cat.[(((triple6) -> rule7))] @2: The mouse is red.[(((((triple6) -> rule7) triple6) -> rule5))] @3: The mouse is young.[(((((((triple6) -> rule7) triple6) -> rule5)) -> rule3))] @4: The mouse likes the cow.[(((((((((triple6) -> rule7) triple6) -> rule5)) -> rule3)) -> rule4))] @5: The mouse chases the mouse.[(((((((((((triple6) -> rule7) triple6) -> rule5)) -> rule3)) -> rule4)) -> rule8))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple2
The cat is rough.
("cat" "is" "rough" "+")
triple3
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
triple4
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple5
The mouse is round.
("mouse" "is" "round" "+")
triple6
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple7
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple8
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
triple9
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple10
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple11
The cat eats the cat.
("cat" "eats" "cat" "+")
((triple3) -> (rule6 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
((triple6) -> (rule7 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
((((triple6) -> (rule7 % int2)) triple6) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
((((((triple6) -> (rule7 % int3)) triple6) -> (rule5 % int2))) -> (rule3 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int3
The mouse likes the cow.
("mouse" "likes" "cow" "+")
((((((((triple6) -> (rule7 % int4)) triple6) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int4
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((((((((((triple6) -> (rule7 % int5)) triple6) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The mouse is red.
("mouse" "is" "red" "+")
int4
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int5