The cat chases the cow. The cat is cold. The cow is young. The cow needs the cat. The cow needs the mouse. The cow sees the cat. The cow sees the mouse. The mouse chases the cat. The mouse is young. The mouse needs the cow. If something is green then it chases the mouse. If something chases the cat and it chases the mouse then the mouse sees the cow. If something sees the mouse then the mouse sees the cat. If something is cold then it needs the mouse. If something is nice and not cold then it does not chase the cat. If something chases the cat then the cat sees the mouse. If something chases the cow then it needs the cow. If something needs the cow then the cow is young.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cow is young.
("cow" "is" "young" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
If something is green then it chases the mouse.
((("something" "is" "green" "+")) -> ("something" "chases" "mouse" "+"))
If something chases the cat and it chases the mouse then the mouse sees the cow.
((("something" "chases" "cat" "+") ("something" "chases" "mouse" "+")) -> ("mouse" "sees" "cow" "+"))
If something sees the mouse then the mouse sees the cat.
((("something" "sees" "mouse" "+")) -> ("mouse" "sees" "cat" "+"))
If something is cold then it needs the mouse.
((("something" "is" "cold" "+")) -> ("something" "needs" "mouse" "+"))
If something is nice and not cold then it does not chase the cat.
((("something" "is" "nice" "+") ("something" "is" "cold" "~")) -> ("something" "chases" "cat" "-"))
If something chases the cat then the cat sees the mouse.
((("something" "chases" "cat" "+")) -> ("cat" "sees" "mouse" "+"))
If something chases the cow then it needs the cow.
((("something" "chases" "cow" "+")) -> ("something" "needs" "cow" "+"))
If something needs the cow then the cow is young.
((("something" "needs" "cow" "+")) -> ("cow" "is" "young" "+"))
The cat is cold.
True
1
proof
[(triple2)]
("cat" "is" "cold" "+")
triple2
The cow is not young.
False
1
inv-proof
[(triple3 OR ((triple10) -> rule8) OR ((((triple1) -> rule7)) -> rule8))]
("cow" "is" "young" "-")
triple3
((triple10) -> (rule8 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
int2
The cat needs the cow.
True
2
proof
[(((triple1) -> rule7))]
("cat" "needs" "cow" "+")
((triple1) -> (rule7 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The cat does not need the mouse.
False
2
inv-proof
[(((triple2) -> rule4))]
("cat" "needs" "mouse" "-")
((triple2) -> (rule4 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The mouse does not chase the mouse.
Unknown
inv-rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "chases" "mouse" "-")
The cat chases the mouse.
Unknown
rconc
[@1: The cat chases the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "chases" "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 young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
@0: The cat chases the cow.[(triple1)] The cat is cold.[(triple2)] The cow is young.[(triple3 OR ((triple10) -> rule8) OR ((((triple1) -> rule7)) -> rule8))] The cow needs the cat.[(triple4)] The cow needs the mouse.[(triple5)] The cow sees the cat.[(triple6)] The cow sees the mouse.[(triple7)] The mouse chases the cat.[(triple8)] The mouse is young.[(triple9)] The mouse needs the cow.[(triple10)] @1: The cat needs the cow.[(((triple1) -> rule7))] The cat needs the mouse.[(((triple2) -> rule4))] The cat sees the mouse.[(((triple8) -> rule6))] The mouse sees the cat.[(((triple7) -> rule3) OR ((((triple8) -> rule6)) -> rule3))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The cow is young.
("cow" "is" "young" "+")
triple3
((triple10) -> (rule8 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
int2
The cow needs the cat.
("cow" "needs" "cat" "+")
triple4
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple5
The cow sees the cat.
("cow" "sees" "cat" "+")
triple6
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple7
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple8
The mouse is young.
("mouse" "is" "young" "+")
triple9
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple10
The cat needs the cow.
("cat" "needs" "cow" "+")
((triple1) -> (rule7 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
((triple2) -> (rule4 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
((triple8) -> (rule6 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
((triple7) -> (rule3 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
((((triple8) -> (rule6 % int2))) -> (rule3 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2