The cow is green. The cow needs the dog. The cow visits the dog. The dog is not kind. The dog needs the cow. The dog sees the cow. The dog visits the cow. If someone sees the dog and they are blue then they visit the cow. If someone is red then they are young. If someone sees the dog then the dog is red. If someone sees the dog and they do not see the cow then the cow visits the dog. If someone needs the cow then they do not need the dog. If the cow sees the dog then the dog is green. If someone is red then they visit the dog. If someone visits the cow then they see the dog.
The cow is green.
("cow" "is" "green" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog is not kind.
("dog" "is" "kind" "-")
The dog needs the cow.
("dog" "needs" "cow" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
If someone sees the dog and they are blue then they visit the cow.
((("someone" "sees" "dog" "+") ("someone" "is" "blue" "+")) -> ("someone" "visits" "cow" "+"))
If someone is red then they are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone sees the dog then the dog is red.
((("someone" "sees" "dog" "+")) -> ("dog" "is" "red" "+"))
If someone sees the dog and they do not see the cow then the cow visits the dog.
((("someone" "sees" "dog" "+") ("someone" "sees" "cow" "~")) -> ("cow" "visits" "dog" "+"))
If someone needs the cow then they do not need the dog.
((("someone" "needs" "cow" "+")) -> ("someone" "needs" "dog" "-"))
If the cow sees the dog then the dog is green.
((("cow" "sees" "dog" "+")) -> ("dog" "is" "green" "+"))
If someone is red then they visit the dog.
((("someone" "is" "red" "+")) -> ("someone" "visits" "dog" "+"))
If someone visits the cow then they see the dog.
((("someone" "visits" "cow" "+")) -> ("someone" "sees" "dog" "+"))
The dog is not kind.
True
1
proof
[(triple4)]
("dog" "is" "kind" "-")
triple4
The cow does not visit the dog.
False
1
inv-proof
[(triple3)]
("cow" "visits" "dog" "-")
triple3
The dog sees the dog.
True
2
proof
[(((triple7) -> rule8))]
("dog" "sees" "dog" "+")
((triple7) -> (rule8 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog does not see the dog.
False
2
inv-proof
[(((triple7) -> rule8))]
("dog" "sees" "dog" "-")
((triple7) -> (rule8 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is red.
True
3
proof
[(((((triple7) -> rule8)) -> rule3))]
("dog" "is" "red" "+")
((((triple7) -> (rule8 % int2))) -> (rule3 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog is not red.
False
3
inv-proof
[(((((triple7) -> rule8)) -> rule3))]
("dog" "is" "red" "-")
((((triple7) -> (rule8 % int2))) -> (rule3 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog is young.
True
4
proof
[(((((((triple7) -> rule8)) -> rule3)) -> rule2))]
("dog" "is" "young" "+")
((((((triple7) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog sees the dog.
("dog" "sees" "dog" "+")
int3
The dog does not visit the dog.
False
4
inv-proof
[(((((((triple7) -> rule8)) -> rule3)) -> rule7))]
("dog" "visits" "dog" "-")
((((((triple7) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog sees the dog.
("dog" "sees" "dog" "+")
int3
The cow does not see the dog.
Unknown
inv-rconc
[@2: The cow sees the dog.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("cow" "sees" "dog" "-")
The cow visits the cow.
Unknown
rconc
[@1: The cow visits the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "visits" "cow" "+")
The cow is not young.
Unknown
inv-rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "young" "-")
The dog is green.
Unknown
rconc
[@3: The dog is green.[CWA. Example of deepest failure = (rule6 <- rule8 <- rule1 <- FAIL)]]
("dog" "is" "green" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
The dog is not blue.
Unknown
inv-random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The cow is green.[(triple1)] The cow needs the dog.[(triple2)] The cow visits the dog.[(triple3)] The dog is not kind.[(triple4)] The dog needs the cow.[(triple5)] The dog sees the cow.[(triple6)] The dog visits the cow.[(triple7)] @1: The dog does not need the dog.[(((triple5) -> rule5))] The dog sees the dog.[(((triple7) -> rule8))] @2: The dog is red.[(((((triple7) -> rule8)) -> rule3))] @3: The dog is young.[(((((((triple7) -> rule8)) -> rule3)) -> rule2))] The dog visits the dog.[(((((((triple7) -> rule8)) -> rule3)) -> rule7))]
The cow is green.
("cow" "is" "green" "+")
triple1
The cow needs the dog.
("cow" "needs" "dog" "+")
triple2
The cow visits the dog.
("cow" "visits" "dog" "+")
triple3
The dog is not kind.
("dog" "is" "kind" "-")
triple4
The dog needs the cow.
("dog" "needs" "cow" "+")
triple5
The dog sees the cow.
("dog" "sees" "cow" "+")
triple6
The dog visits the cow.
("dog" "visits" "cow" "+")
triple7
The dog does not need the dog.
("dog" "needs" "dog" "-")
((triple5) -> (rule5 % int1))
The dog does not need the dog.
("dog" "needs" "dog" "-")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
((triple7) -> (rule8 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
((((triple7) -> (rule8 % int2))) -> (rule3 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog is young.
("dog" "is" "young" "+")
((((((triple7) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog sees the dog.
("dog" "sees" "dog" "+")
int3
The dog visits the dog.
("dog" "visits" "dog" "+")
((((((triple7) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog sees the dog.
("dog" "sees" "dog" "+")
int3