The cat chases the mouse. The mouse chases the cat. The mouse visits the cat. If the cat chases the mouse then the mouse chases the cat. If the cat visits the mouse then the mouse sees the cat. If someone is red then they chase the mouse. If someone is round then they chase the cat. If someone visits the cat then the cat visits the mouse. If someone chases the mouse and they visit the cat then the cat visits the mouse. If someone chases the cat and they see the cat then they are cold. If someone visits the mouse then the mouse chases the cat.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
If the cat chases the mouse then the mouse chases the cat.
((("cat" "chases" "mouse" "+")) -> ("mouse" "chases" "cat" "+"))
If the cat visits the mouse then the mouse sees the cat.
((("cat" "visits" "mouse" "+")) -> ("mouse" "sees" "cat" "+"))
If someone is red then they chase the mouse.
((("someone" "is" "red" "+")) -> ("someone" "chases" "mouse" "+"))
If someone is round then they chase the cat.
((("someone" "is" "round" "+")) -> ("someone" "chases" "cat" "+"))
If someone visits the cat then the cat visits the mouse.
((("someone" "visits" "cat" "+")) -> ("cat" "visits" "mouse" "+"))
If someone chases the mouse and they visit the cat then the cat visits the mouse.
((("someone" "chases" "mouse" "+") ("someone" "visits" "cat" "+")) -> ("cat" "visits" "mouse" "+"))
If someone chases the cat and they see the cat then they are cold.
((("someone" "chases" "cat" "+") ("someone" "sees" "cat" "+")) -> ("someone" "is" "cold" "+"))
If someone visits the mouse then the mouse chases the cat.
((("someone" "visits" "mouse" "+")) -> ("mouse" "chases" "cat" "+"))
The mouse chases the cat.
True
1
proof
[(triple2 OR ((triple1) -> rule1) OR ((((triple3) -> rule5)) -> rule8))]
("mouse" "chases" "cat" "+")
triple2
((triple1) -> (rule1 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule8 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The cat does not chase the mouse.
False
1
inv-proof
[(triple1)]
("cat" "chases" "mouse" "-")
triple1
The cat visits the mouse.
True
2
proof
[(((triple3) -> rule5))]
("cat" "visits" "mouse" "+")
((triple3) -> (rule5 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat does not visit the mouse.
False
2
inv-proof
[(((triple3) -> rule5))]
("cat" "visits" "mouse" "-")
((triple3) -> (rule5 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The mouse sees the cat.
True
3
proof
[(((((triple3) -> rule5)) -> rule2))]
("mouse" "sees" "cat" "+")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The mouse does not see the cat.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule2))]
("mouse" "sees" "cat" "-")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The mouse is cold.
True
5
proof
[(((triple2 ((((triple3) -> rule5)) -> rule2)) -> rule7) OR ((((triple1) -> rule1) ((((triple3) -> rule5)) -> rule2)) -> rule7) OR ((((((triple3) -> rule5)) -> rule8) ((((triple3) -> rule5)) -> rule2)) -> rule7))]
("mouse" "is" "cold" "+")
((triple2 ((((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int3
((((triple1) -> (rule1 % int4)) ((((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int3
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int4
((((((triple3) -> (rule5 % int4))) -> (rule8 % int3)) ((((triple3) -> (rule5 % int4))) -> (rule2 % int2))) -> (rule7 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int3
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int4
The mouse is not cold.
False
5
inv-proof
[(((triple2 ((((triple3) -> rule5)) -> rule2)) -> rule7) OR ((((triple1) -> rule1) ((((triple3) -> rule5)) -> rule2)) -> rule7) OR ((((((triple3) -> rule5)) -> rule8) ((((triple3) -> rule5)) -> rule2)) -> rule7))]
("mouse" "is" "cold" "-")
((triple2 ((((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int3
((((triple1) -> (rule1 % int4)) ((((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int3
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int4
((((((triple3) -> (rule5 % int4))) -> (rule8 % int3)) ((((triple3) -> (rule5 % int4))) -> (rule2 % int2))) -> (rule7 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int3
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int4
The cat does not chase the cat.
Unknown
inv-rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "chases" "cat" "-")
The mouse chases the mouse.
Unknown
rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "chases" "mouse" "+")
The cat is not cold.
Unknown
inv-rconc
[@1: The cat is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "is" "cold" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
The cat is not round.
Unknown
inv-random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
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 cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
@0: The cat chases the mouse.[(triple1)] The mouse chases the cat.[(triple2 OR ((triple1) -> rule1) OR ((((triple3) -> rule5)) -> rule8))] The mouse visits the cat.[(triple3)] @1: The cat visits the mouse.[(((triple3) -> rule5))] @2: The mouse sees the cat.[(((((triple3) -> rule5)) -> rule2))] @3: The mouse is cold.[(((triple2 ((((triple3) -> rule5)) -> rule2)) -> rule7) OR ((((triple1) -> rule1) ((((triple3) -> rule5)) -> rule2)) -> rule7) OR ((((((triple3) -> rule5)) -> rule8) ((((triple3) -> rule5)) -> rule2)) -> rule7))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple2
((triple1) -> (rule1 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule8 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple3
The cat visits the mouse.
("cat" "visits" "mouse" "+")
((triple3) -> (rule5 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
((triple2 ((((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int3
((((triple1) -> (rule1 % int4)) ((((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int3
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int4
((((((triple3) -> (rule5 % int4))) -> (rule8 % int3)) ((((triple3) -> (rule5 % int4))) -> (rule2 % int2))) -> (rule7 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int3
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int4