The cow is nice. The cow visits the rabbit. The rabbit chases the cow. The rabbit is cold. The rabbit is green. The rabbit sees the cow. The rabbit visits the cow. If something sees the cow then the cow chases the rabbit. If something is green then it visits the cow. If something chases the rabbit then it chases the cow. If something is nice then it is rough. If something chases the rabbit and the rabbit chases the cow then it is green. If the rabbit is cold and the rabbit chases the cow then the rabbit visits the cow.
The cow is nice.
("cow" "is" "nice" "+")
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
If something sees the cow then the cow chases the rabbit.
((("something" "sees" "cow" "+")) -> ("cow" "chases" "rabbit" "+"))
If something is green then it visits the cow.
((("something" "is" "green" "+")) -> ("something" "visits" "cow" "+"))
If something chases the rabbit then it chases the cow.
((("something" "chases" "rabbit" "+")) -> ("something" "chases" "cow" "+"))
If something is nice then it is rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If something chases the rabbit and the rabbit chases the cow then it is green.
((("something" "chases" "rabbit" "+") ("rabbit" "chases" "cow" "+")) -> ("something" "is" "green" "+"))
If the rabbit is cold and the rabbit chases the cow then the rabbit visits the cow.
((("rabbit" "is" "cold" "+") ("rabbit" "chases" "cow" "+")) -> ("rabbit" "visits" "cow" "+"))
The cow visits the rabbit.
True
1
proof
[(triple2)]
("cow" "visits" "rabbit" "+")
triple2
The cow does not visit the rabbit.
False
1
inv-proof
[(triple2)]
("cow" "visits" "rabbit" "-")
triple2
The cow chases the rabbit.
True
2
proof
[(((triple6) -> rule1))]
("cow" "chases" "rabbit" "+")
((triple6) -> (rule1 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The cow is not rough.
False
2
inv-proof
[(((triple1) -> rule4))]
("cow" "is" "rough" "-")
((triple1) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow chases the cow.
True
3
proof
[(((((triple6) -> rule1)) -> rule3))]
("cow" "chases" "cow" "+")
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
The cow is not green.
False
4
inv-proof
[(((((triple6) -> rule1) triple3) -> rule5))]
("cow" "is" "green" "-")
((((triple6) -> (rule1 % int2)) triple3) -> (rule5 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
The rabbit is not rough.
Unknown
inv-rconc
[@1: The rabbit is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "is" "rough" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The rabbit is young.
Unknown
random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "+")
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
@0: The cow is nice.[(triple1)] The cow visits the rabbit.[(triple2)] The rabbit chases the cow.[(triple3)] The rabbit is cold.[(triple4)] The rabbit is green.[(triple5)] The rabbit sees the cow.[(triple6)] The rabbit visits the cow.[(triple7 OR ((triple5) -> rule2) OR ((triple4 triple3) -> rule6))] @1: The cow chases the rabbit.[(((triple6) -> rule1))] The cow is rough.[(((triple1) -> rule4))] @2: The cow chases the cow.[(((((triple6) -> rule1)) -> rule3))] The cow is green.[(((((triple6) -> rule1) triple3) -> rule5))] @3: The cow visits the cow.[(((((((triple6) -> rule1) triple3) -> rule5)) -> rule2))]
The cow is nice.
("cow" "is" "nice" "+")
triple1
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
triple2
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
triple3
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple4
The rabbit is green.
("rabbit" "is" "green" "+")
triple5
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple6
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple7
((triple5) -> (rule2 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
((triple4 triple3) -> (rule6 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
((triple6) -> (rule1 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
((triple1) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
The cow is green.
("cow" "is" "green" "+")
((((triple6) -> (rule1 % int2)) triple3) -> (rule5 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
((((((triple6) -> (rule1 % int3)) triple3) -> (rule5 % int2))) -> (rule2 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int3