The cow sees the dog. The dog chases the cow. The dog is green. If someone chases the dog then the dog does not visit the cow. If someone is green then they chase the dog. If someone chases the dog then the dog is rough. If someone sees the dog and the dog is cold then they visit the cow. If someone is nice and they do not chase the dog then the dog is nice. If someone sees the cow then they are cold. If someone sees the dog then the dog sees the cow. If someone sees the cow and they do not chase the dog then the dog does not see the cow.
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The dog is green.
("dog" "is" "green" "+")
If someone chases the dog then the dog does not visit the cow.
((("someone" "chases" "dog" "+")) -> ("dog" "visits" "cow" "-"))
If someone is green then they chase the dog.
((("someone" "is" "green" "+")) -> ("someone" "chases" "dog" "+"))
If someone chases the dog then the dog is rough.
((("someone" "chases" "dog" "+")) -> ("dog" "is" "rough" "+"))
If someone sees the dog and the dog is cold then they visit the cow.
((("someone" "sees" "dog" "+") ("dog" "is" "cold" "+")) -> ("someone" "visits" "cow" "+"))
If someone is nice and they do not chase the dog then the dog is nice.
((("someone" "is" "nice" "+") ("someone" "chases" "dog" "~")) -> ("dog" "is" "nice" "+"))
If someone sees the cow then they are cold.
((("someone" "sees" "cow" "+")) -> ("someone" "is" "cold" "+"))
If someone sees the dog then the dog sees the cow.
((("someone" "sees" "dog" "+")) -> ("dog" "sees" "cow" "+"))
If someone sees the cow and they do not chase the dog then the dog does not see the cow.
((("someone" "sees" "cow" "+") ("someone" "chases" "dog" "~")) -> ("dog" "sees" "cow" "-"))
The dog is green.
True
1
proof
[(triple3)]
("dog" "is" "green" "+")
triple3
The cow does not see the dog.
False
1
inv-proof
[(triple1)]
("cow" "sees" "dog" "-")
triple1
The dog chases the dog.
True
2
proof
[(((triple3) -> rule2))]
("dog" "chases" "dog" "+")
((triple3) -> (rule2 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog does not chase the dog.
False
2
inv-proof
[(((triple3) -> rule2))]
("dog" "chases" "dog" "-")
((triple3) -> (rule2 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog does not visit the cow.
True
3
proof
[(((((triple3) -> rule2)) -> rule1))]
("dog" "visits" "cow" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The dog does not visit the cow.
("dog" "visits" "cow" "-")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog is not rough.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("dog" "is" "rough" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The cow visits the cow.
True
5
proof
[(((triple1 ((((triple1) -> rule7)) -> rule6)) -> rule4))]
("cow" "visits" "cow" "+")
((triple1 ((((triple1) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The dog sees the cow.
("dog" "sees" "cow" "+")
int3
The cow does not visit the cow.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule7)) -> rule6)) -> rule4))]
("cow" "visits" "cow" "-")
((triple1 ((((triple1) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The dog sees the cow.
("dog" "sees" "cow" "+")
int3
The dog is not nice.
Unknown
inv-rconc
[@1: The dog is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "nice" "-")
The cow is cold.
Unknown
rconc
[@1: The cow is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "is" "cold" "+")
The cow does not chase the dog.
Unknown
inv-rconc
[@1: The cow chases the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "chases" "dog" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
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 cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
The cow is not nice.
Unknown
inv-random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The cow sees the dog.[(triple1)] The dog chases the cow.[(triple2)] The dog is green.[(triple3)] @1: The dog chases the dog.[(((triple3) -> rule2))] The dog sees the cow.[(((triple1) -> rule7))] @2: The dog does not visit the cow.[(((((triple3) -> rule2)) -> rule1))] The dog is cold.[(((((triple1) -> rule7)) -> rule6))] The dog is rough.[(((((triple3) -> rule2)) -> rule3))] @3: The cow visits the cow.[(((triple1 ((((triple1) -> rule7)) -> rule6)) -> rule4))]
The cow sees the dog.
("cow" "sees" "dog" "+")
triple1
The dog chases the cow.
("dog" "chases" "cow" "+")
triple2
The dog is green.
("dog" "is" "green" "+")
triple3
The dog chases the dog.
("dog" "chases" "dog" "+")
((triple3) -> (rule2 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog sees the cow.
("dog" "sees" "cow" "+")
((triple1) -> (rule7 % int1))
The dog sees the cow.
("dog" "sees" "cow" "+")
int1
The dog does not visit the cow.
("dog" "visits" "cow" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The dog does not visit the cow.
("dog" "visits" "cow" "-")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog sees the cow.
("dog" "sees" "cow" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
((triple1 ((((triple1) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The dog sees the cow.
("dog" "sees" "cow" "+")
int3