The cow is green. The tiger sees the cow. The tiger visits the cow. If something is round then it sees the tiger. If something visits the cow then the cow does not visit the tiger. Round things are nice.
The cow is green.
("cow" "is" "green" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If something is round then it sees the tiger.
((("something" "is" "round" "+")) -> ("something" "sees" "tiger" "+"))
If something visits the cow then the cow does not visit the tiger.
((("something" "visits" "cow" "+")) -> ("cow" "visits" "tiger" "-"))
Round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
The tiger visits the cow.
True
1
proof
[(triple3)]
("tiger" "visits" "cow" "+")
triple3
The tiger does not visit the cow.
False
1
inv-proof
[(triple3)]
("tiger" "visits" "cow" "-")
triple3
The cow does not visit the tiger.
True
2
proof
[(((triple3) -> rule2))]
("cow" "visits" "tiger" "-")
((triple3) -> (rule2 % int1))
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
int1
The cow visits the tiger.
False
2
inv-proof
[(((triple3) -> rule2))]
("cow" "visits" "tiger" "+")
((triple3) -> (rule2 % int1))
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
int1
The cow is not nice.
Unknown
inv-rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "nice" "-")
The cow sees the tiger.
Unknown
rconc
[@1: The cow sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "sees" "tiger" "+")
The cow does not need the tiger.
Unknown
inv-random
[@0: The cow needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "tiger" "-")
The cow is kind.
Unknown
random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "+")
@0: The cow is green.[(triple1)] The tiger sees the cow.[(triple2)] The tiger visits the cow.[(triple3)] @1: The cow does not visit the tiger.[(((triple3) -> rule2))]
The cow is green.
("cow" "is" "green" "+")
triple1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple2
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple3
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
((triple3) -> (rule2 % int1))
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
int1