The cow visits the rabbit. The rabbit chases the cow. The squirrel visits the cow. If something visits the squirrel then it does not visit the rabbit. If something visits the squirrel then it is young. If something is green then it visits the cow. If something visits the rabbit then it is green. If something visits the cow then it chases the squirrel. If something likes the squirrel and it is not young then the squirrel is not rough.
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
If something visits the squirrel then it does not visit the rabbit.
((("something" "visits" "squirrel" "+")) -> ("something" "visits" "rabbit" "-"))
If something visits the squirrel then it is young.
((("something" "visits" "squirrel" "+")) -> ("something" "is" "young" "+"))
If something is green then it visits the cow.
((("something" "is" "green" "+")) -> ("something" "visits" "cow" "+"))
If something visits the rabbit then it is green.
((("something" "visits" "rabbit" "+")) -> ("something" "is" "green" "+"))
If something visits the cow then it chases the squirrel.
((("something" "visits" "cow" "+")) -> ("something" "chases" "squirrel" "+"))
If something likes the squirrel and it is not young then the squirrel is not rough.
((("something" "likes" "squirrel" "+") ("something" "is" "young" "~")) -> ("squirrel" "is" "rough" "-"))
The rabbit chases the cow.
True
1
proof
[(triple2)]
("rabbit" "chases" "cow" "+")
triple2
The squirrel does not visit the cow.
False
1
inv-proof
[(triple3)]
("squirrel" "visits" "cow" "-")
triple3
The cow is green.
True
2
proof
[(((triple1) -> rule4))]
("cow" "is" "green" "+")
((triple1) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The squirrel does not chase the squirrel.
False
2
inv-proof
[(((triple3) -> rule5))]
("squirrel" "chases" "squirrel" "-")
((triple3) -> (rule5 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The cow visits the cow.
True
3
proof
[(((((triple1) -> rule4)) -> rule3))]
("cow" "visits" "cow" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow does not visit the cow.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule3))]
("cow" "visits" "cow" "-")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow chases the squirrel.
True
4
proof
[(((((((triple1) -> rule4)) -> rule3)) -> rule5))]
("cow" "chases" "squirrel" "+")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
The cow does not chase the squirrel.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule3)) -> rule5))]
("cow" "chases" "squirrel" "-")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
The rabbit does not visit the cow.
Unknown
inv-rconc
[@2: The rabbit visits the cow.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("rabbit" "visits" "cow" "-")
The rabbit is green.
Unknown
rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "is" "green" "+")
The rabbit does not chase the squirrel.
Unknown
inv-rconc
[@3: The rabbit chases the squirrel.[CWA. Example of deepest failure = (rule5 <- rule3 <- rule4 <- FAIL)]]
("rabbit" "chases" "squirrel" "-")
The squirrel is green.
Unknown
rconc
[@1: The squirrel is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "is" "green" "+")
The cow does not like the cow.
Unknown
inv-random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
@0: The cow visits the rabbit.[(triple1)] The rabbit chases the cow.[(triple2)] The squirrel visits the cow.[(triple3)] @1: The cow is green.[(((triple1) -> rule4))] The squirrel chases the squirrel.[(((triple3) -> rule5))] @2: The cow visits the cow.[(((((triple1) -> rule4)) -> rule3))] @3: The cow chases the squirrel.[(((((((triple1) -> rule4)) -> rule3)) -> rule5))]
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
triple1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
triple2
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple3
The cow is green.
("cow" "is" "green" "+")
((triple1) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((triple3) -> (rule5 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3