The cat is blue. The cat is not rough. The cat does not visit the cow. The cow chases the cat. The cow sees the cat. The mouse chases the cat. The mouse is blue. The mouse is nice. The mouse sees the cat. The mouse visits the cat. If something chases the mouse and the mouse sees the cat then it does not chase the cow. If something chases the cat then it chases the cow. If something is big then it visits the mouse. If the mouse visits the cow then the mouse sees the cat. If something chases the cat and it chases the cow then the cat is big. If something is nice and it does not visit the cow then it is round.
The cat is blue.
("cat" "is" "blue" "+")
The cat is not rough.
("cat" "is" "rough" "-")
The cat does not visit the cow.
("cat" "visits" "cow" "-")
The cow chases the cat.
("cow" "chases" "cat" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
If something chases the mouse and the mouse sees the cat then it does not chase the cow.
((("something" "chases" "mouse" "+") ("mouse" "sees" "cat" "+")) -> ("something" "chases" "cow" "-"))
If something chases the cat then it chases the cow.
((("something" "chases" "cat" "+")) -> ("something" "chases" "cow" "+"))
If something is big then it visits the mouse.
((("something" "is" "big" "+")) -> ("something" "visits" "mouse" "+"))
If the mouse visits the cow then the mouse sees the cat.
((("mouse" "visits" "cow" "+")) -> ("mouse" "sees" "cat" "+"))
If something chases the cat and it chases the cow then the cat is big.
((("something" "chases" "cat" "+") ("something" "chases" "cow" "+")) -> ("cat" "is" "big" "+"))
If something is nice and it does not visit the cow then it is round.
((("something" "is" "nice" "+") ("something" "visits" "cow" "~")) -> ("something" "is" "round" "+"))
The mouse is nice.
True
1
proof
[(triple8)]
("mouse" "is" "nice" "+")
triple8
The mouse does not see the cat.
False
1
inv-proof
[(triple9)]
("mouse" "sees" "cat" "-")
triple9
The cow chases the cow.
True
2
proof
[(((triple4) -> rule2))]
("cow" "chases" "cow" "+")
((triple4) -> (rule2 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The mouse does not chase the cow.
False
2
inv-proof
[(((triple6) -> rule2))]
("mouse" "chases" "cow" "-")
((triple6) -> (rule2 % int1))
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int1
The cat is big.
True
4
proof
[(((triple4 ((triple4) -> rule2)) -> rule5) OR ((triple6 ((triple6) -> rule2)) -> rule5))]
("cat" "is" "big" "+")
((triple4 ((triple4) -> (rule2 % int2))) -> (rule5 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
((triple6 ((triple6) -> (rule2 % int2))) -> (rule5 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int2
The cat is not big.
False
4
inv-proof
[(((triple4 ((triple4) -> rule2)) -> rule5) OR ((triple6 ((triple6) -> rule2)) -> rule5))]
("cat" "is" "big" "-")
((triple4 ((triple4) -> (rule2 % int2))) -> (rule5 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
((triple6 ((triple6) -> (rule2 % int2))) -> (rule5 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int2
The cat visits the mouse.
True
5
proof
[(((((triple4 ((triple4) -> rule2)) -> rule5)) -> rule3) OR ((((triple6 ((triple6) -> rule2)) -> rule5)) -> rule3))]
("cat" "visits" "mouse" "+")
((((triple4 ((triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cow chases the cow.
("cow" "chases" "cow" "+")
int3
((((triple6 ((triple6) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int3
The cat does not visit the mouse.
False
5
inv-proof
[(((((triple4 ((triple4) -> rule2)) -> rule5)) -> rule3) OR ((((triple6 ((triple6) -> rule2)) -> rule5)) -> rule3))]
("cat" "visits" "mouse" "-")
((((triple4 ((triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cow chases the cow.
("cow" "chases" "cow" "+")
int3
((((triple6 ((triple6) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int3
The cow does not visit the mouse.
Unknown
inv-rconc
[@1: The cow visits the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "visits" "mouse" "-")
The mouse is round.
Unknown
rconc
[@1: The mouse is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "round" "+")
The cat does not chase the cow.
Unknown
inv-rconc
[@1: The cat chases the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "chases" "cow" "-")
The mouse visits the mouse.
Unknown
rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "visits" "mouse" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cow is blue.
Unknown
random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The cow sees the mouse.
Unknown
random
[@0: The cow sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "mouse" "+")
@0: The cat does not visit the cow.[(triple3)] The cat is blue.[(triple1)] The cat is not rough.[(triple2)] The cow chases the cat.[(triple4)] The cow sees the cat.[(triple5)] The mouse chases the cat.[(triple6)] The mouse is blue.[(triple7)] The mouse is nice.[(triple8)] The mouse sees the cat.[(triple9)] The mouse visits the cat.[(triple10)] @1: The cow chases the cow.[(((triple4) -> rule2))] The mouse chases the cow.[(((triple6) -> rule2))] @2: The cat is big.[(((triple4 ((triple4) -> rule2)) -> rule5) OR ((triple6 ((triple6) -> rule2)) -> rule5))] @3: The cat visits the mouse.[(((((triple4 ((triple4) -> rule2)) -> rule5)) -> rule3) OR ((((triple6 ((triple6) -> rule2)) -> rule5)) -> rule3))]
The cat does not visit the cow.
("cat" "visits" "cow" "-")
triple3
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat is not rough.
("cat" "is" "rough" "-")
triple2
The cow chases the cat.
("cow" "chases" "cat" "+")
triple4
The cow sees the cat.
("cow" "sees" "cat" "+")
triple5
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple6
The mouse is blue.
("mouse" "is" "blue" "+")
triple7
The mouse is nice.
("mouse" "is" "nice" "+")
triple8
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple9
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple10
The cow chases the cow.
("cow" "chases" "cow" "+")
((triple4) -> (rule2 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
((triple6) -> (rule2 % int1))
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int1
The cat is big.
("cat" "is" "big" "+")
((triple4 ((triple4) -> (rule2 % int2))) -> (rule5 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
((triple6 ((triple6) -> (rule2 % int2))) -> (rule5 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int2
The cat visits the mouse.
("cat" "visits" "mouse" "+")
((((triple4 ((triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cow chases the cow.
("cow" "chases" "cow" "+")
int3
((((triple6 ((triple6) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int3