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