The cow is green. The rabbit sees the cow. If something chases the rabbit and the rabbit is young then the rabbit needs the cow. If something chases the cow then it is green. If something sees the cow then it needs the cow. If something needs the rabbit then it sees the cow. If something needs the rabbit then it chases the cow. If something sees the rabbit then it sees the cow. If something chases the rabbit then the rabbit is green. All green things are young.
The cow is green.
("cow" "is" "green" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
If something chases the rabbit and the rabbit is young then the rabbit needs the cow.
((("something" "chases" "rabbit" "+") ("rabbit" "is" "young" "+")) -> ("rabbit" "needs" "cow" "+"))
If something chases the cow then it is green.
((("something" "chases" "cow" "+")) -> ("something" "is" "green" "+"))
If something sees the cow then it needs the cow.
((("something" "sees" "cow" "+")) -> ("something" "needs" "cow" "+"))
If something needs the rabbit then it sees the cow.
((("something" "needs" "rabbit" "+")) -> ("something" "sees" "cow" "+"))
If something needs the rabbit then it chases the cow.
((("something" "needs" "rabbit" "+")) -> ("something" "chases" "cow" "+"))
If something sees the rabbit then it sees the cow.
((("something" "sees" "rabbit" "+")) -> ("something" "sees" "cow" "+"))
If something chases the rabbit then the rabbit is green.
((("something" "chases" "rabbit" "+")) -> ("rabbit" "is" "green" "+"))
All green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
The rabbit sees the cow.
True
1
proof
[(triple2)]
("rabbit" "sees" "cow" "+")
triple2
The cow is not green.
False
1
inv-proof
[(triple1)]
("cow" "is" "green" "-")
triple1
The cow is young.
True
2
proof
[(((triple1) -> rule8))]
("cow" "is" "young" "+")
((triple1) -> (rule8 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is not young.
False
2
inv-proof
[(((triple1) -> rule8))]
("cow" "is" "young" "-")
((triple1) -> (rule8 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The rabbit does not chase the cow.
Unknown
inv-rconc
[@1: The rabbit chases the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "chases" "cow" "-")
The cow chases the cow.
Unknown
rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "chases" "cow" "+")
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The cow sees the rabbit.
Unknown
random
[@0: The cow sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "rabbit" "+")
@0: The cow is green.[(triple1)] The rabbit sees the cow.[(triple2)] @1: The cow is young.[(((triple1) -> rule8))] The rabbit needs the cow.[(((triple2) -> rule3))]
The cow is green.
("cow" "is" "green" "+")
triple1
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple2
The cow is young.
("cow" "is" "young" "+")
((triple1) -> (rule8 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
((triple2) -> (rule3 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1