The cow is young. The dog visits the cow. The tiger is blue. If something visits the cow and it sees the cow then it is round. If something chases the tiger and it chases the dog then the dog chases the cow. If something visits the cow then the cow visits the dog. If the tiger sees the cow and the cow chases the dog then the dog chases the cow. If something is round and blue then it visits the dog. If something visits the dog then it visits the cow.
The cow is young.
("cow" "is" "young" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
If something visits the cow and it sees the cow then it is round.
((("something" "visits" "cow" "+") ("something" "sees" "cow" "+")) -> ("something" "is" "round" "+"))
If something chases the tiger and it chases the dog then the dog chases the cow.
((("something" "chases" "tiger" "+") ("something" "chases" "dog" "+")) -> ("dog" "chases" "cow" "+"))
If something visits the cow then the cow visits the dog.
((("something" "visits" "cow" "+")) -> ("cow" "visits" "dog" "+"))
If the tiger sees the cow and the cow chases the dog then the dog chases the cow.
((("tiger" "sees" "cow" "+") ("cow" "chases" "dog" "+")) -> ("dog" "chases" "cow" "+"))
If something is round and blue then it visits the dog.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "visits" "dog" "+"))
If something visits the dog then it visits the cow.
((("something" "visits" "dog" "+")) -> ("something" "visits" "cow" "+"))
The tiger is blue.
True
1
proof
[(triple3)]
("tiger" "is" "blue" "+")
triple3
The dog does not visit the cow.
False
1
inv-proof
[(triple2)]
("dog" "visits" "cow" "-")
triple2
The cow visits the dog.
True
2
proof
[(((triple2) -> rule3))]
("cow" "visits" "dog" "+")
((triple2) -> (rule3 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow does not visit the dog.
False
2
inv-proof
[(((triple2) -> rule3))]
("cow" "visits" "dog" "-")
((triple2) -> (rule3 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The dog does not chase the cow.
Unknown
inv-rconc
[@1: The dog chases the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "chases" "cow" "-")
The dog visits the dog.
Unknown
rconc
[@1: The dog visits the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "visits" "dog" "+")
The dog does not see the cow.
Unknown
inv-random
[@0: The dog sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "cow" "-")
The dog is rough.
Unknown
random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "+")
@0: The cow is young.[(triple1)] The dog visits the cow.[(triple2)] The tiger is blue.[(triple3)] @1: The cow visits the dog.[(((triple2) -> rule3))] @2: The cow visits the cow.[(((((triple2) -> rule3)) -> rule6))]
The cow is young.
("cow" "is" "young" "+")
triple1
The dog visits the cow.
("dog" "visits" "cow" "+")
triple2
The tiger is blue.
("tiger" "is" "blue" "+")
triple3
The cow visits the dog.
("cow" "visits" "dog" "+")
((triple2) -> (rule3 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
int2