The cat is big. The cat is blue. The cat is green. The cat is young. The cat sees the mouse. The cat visits the mouse. The mouse chases the cat. The mouse is big. The mouse is green. The mouse sees the cat. If something visits the mouse then it chases the mouse. Young things are green. If something is green then it sees the cat. If something sees the mouse then it visits the mouse. If something sees the mouse and the mouse visits the cat then the mouse is young. If the mouse sees the cat then the mouse chases the cat.
The cat is big.
("cat" "is" "big" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is young.
("cat" "is" "young" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
If something visits the mouse then it chases the mouse.
((("something" "visits" "mouse" "+")) -> ("something" "chases" "mouse" "+"))
Young things are green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If something is green then it sees the cat.
((("something" "is" "green" "+")) -> ("something" "sees" "cat" "+"))
If something sees the mouse then it visits the mouse.
((("something" "sees" "mouse" "+")) -> ("something" "visits" "mouse" "+"))
If something sees the mouse and the mouse visits the cat then the mouse is young.
((("something" "sees" "mouse" "+") ("mouse" "visits" "cat" "+")) -> ("mouse" "is" "young" "+"))
If the mouse sees the cat then the mouse chases the cat.
((("mouse" "sees" "cat" "+")) -> ("mouse" "chases" "cat" "+"))
The mouse is green.
True
1
proof
[(triple9)]
("mouse" "is" "green" "+")
triple9
The mouse is not big.
False
1
inv-proof
[(triple8)]
("mouse" "is" "big" "-")
triple8
The cat sees the cat.
True
2
proof
[(((triple3) -> rule3) OR ((((triple4) -> rule2)) -> rule3))]
("cat" "sees" "cat" "+")
((triple3) -> (rule3 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat does not see the cat.
False
2
inv-proof
[(((triple3) -> rule3) OR ((((triple4) -> rule2)) -> rule3))]
("cat" "sees" "cat" "-")
((triple3) -> (rule3 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The mouse is not young.
Unknown
inv-rconc
[@1: The mouse is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "young" "-")
The mouse chases the mouse.
Unknown
rconc
[@2: The mouse chases the mouse.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("mouse" "chases" "mouse" "+")
The cat is not red.
Unknown
inv-random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The cat is big.[(triple1)] The cat is blue.[(triple2)] The cat is green.[(triple3 OR ((triple4) -> rule2))] The cat is young.[(triple4)] The cat sees the mouse.[(triple5)] The cat visits the mouse.[(triple6 OR ((triple5) -> rule4))] The mouse chases the cat.[(triple7 OR ((triple10) -> rule6) OR ((((triple9) -> rule3)) -> rule6))] The mouse is big.[(triple8)] The mouse is green.[(triple9)] The mouse sees the cat.[(triple10 OR ((triple9) -> rule3))] @1: The cat chases the mouse.[(((triple6) -> rule1) OR ((((triple5) -> rule4)) -> rule1))] The cat sees the cat.[(((triple3) -> rule3) OR ((((triple4) -> rule2)) -> rule3))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat is green.
("cat" "is" "green" "+")
triple3
((triple4) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is young.
("cat" "is" "young" "+")
triple4
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple5
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple6
((triple5) -> (rule4 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple7
((triple10) -> (rule6 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
((((triple9) -> (rule3 % int2))) -> (rule6 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
triple8
The mouse is green.
("mouse" "is" "green" "+")
triple9
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple10
((triple9) -> (rule3 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
((triple6) -> (rule1 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule1 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple3) -> (rule3 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2