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