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