The cow sees the dog. The dog is blue. The dog is young. The dog does not see the cow. The tiger eats the cow. The tiger eats the dog. The tiger is blue. The tiger is cold. The tiger is round. The tiger sees the cow. The tiger visits the cow. The tiger visits the dog. If something visits the dog and it is big then it does not eat the tiger. If something sees the cow then the cow visits the dog. If the tiger visits the cow and the tiger is cold then the cow eats the tiger. If something sees the tiger and it is not big then it sees the cow. If something eats the tiger then it eats the dog. If something eats the tiger then it visits the cow.
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is young.
("dog" "is" "young" "+")
The dog does not see the cow.
("dog" "sees" "cow" "-")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger eats the dog.
("tiger" "eats" "dog" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If something visits the dog and it is big then it does not eat the tiger.
((("something" "visits" "dog" "+") ("something" "is" "big" "+")) -> ("something" "eats" "tiger" "-"))
If something sees the cow then the cow visits the dog.
((("something" "sees" "cow" "+")) -> ("cow" "visits" "dog" "+"))
If the tiger visits the cow and the tiger is cold then the cow eats the tiger.
((("tiger" "visits" "cow" "+") ("tiger" "is" "cold" "+")) -> ("cow" "eats" "tiger" "+"))
If something sees the tiger and it is not big then it sees the cow.
((("something" "sees" "tiger" "+") ("something" "is" "big" "~")) -> ("something" "sees" "cow" "+"))
If something eats the tiger then it eats the dog.
((("something" "eats" "tiger" "+")) -> ("something" "eats" "dog" "+"))
If something eats the tiger then it visits the cow.
((("something" "eats" "tiger" "+")) -> ("something" "visits" "cow" "+"))
The dog is blue.
True
1
proof
[(triple2)]
("dog" "is" "blue" "+")
triple2
The tiger does not see the cow.
False
1
inv-proof
[(triple10)]
("tiger" "sees" "cow" "-")
triple10
The cow visits the dog.
True
2
proof
[(((triple10) -> rule2))]
("cow" "visits" "dog" "+")
((triple10) -> (rule2 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow does not eat the tiger.
False
3
inv-proof
[(((triple11 triple8) -> rule3))]
("cow" "eats" "tiger" "-")
((triple11 triple8) -> (rule3 % int1))
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int1
The cow eats the dog.
True
4
proof
[(((((triple11 triple8) -> rule3)) -> rule5))]
("cow" "eats" "dog" "+")
((((triple11 triple8) -> (rule3 % int2))) -> (rule5 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int2
The cow does not eat the dog.
False
4
inv-proof
[(((((triple11 triple8) -> rule3)) -> rule5))]
("cow" "eats" "dog" "-")
((((triple11 triple8) -> (rule3 % int2))) -> (rule5 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int2
The cow does not see the cow.
Unknown
inv-rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "sees" "cow" "-")
The dog eats the dog.
Unknown
rconc
[@1: The dog eats the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "eats" "dog" "+")
The dog does not visit the cow.
Unknown
inv-rconc
[@1: The dog visits the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "visits" "cow" "-")
The cow sees the tiger.
Unknown
random
[@0: The cow sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "tiger" "+")
The cow does not eat the cow.
Unknown
inv-random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "-")
The cow is round.
Unknown
random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "+")
@0: The cow sees the dog.[(triple1)] The dog does not see the cow.[(triple4)] The dog is blue.[(triple2)] The dog is young.[(triple3)] The tiger eats the cow.[(triple5)] The tiger eats the dog.[(triple6)] The tiger is blue.[(triple7)] The tiger is cold.[(triple8)] The tiger is round.[(triple9)] The tiger sees the cow.[(triple10)] The tiger visits the cow.[(triple11)] The tiger visits the dog.[(triple12)] @1: The cow eats the tiger.[(((triple11 triple8) -> rule3))] The cow visits the dog.[(((triple10) -> rule2))] @2: The cow eats the dog.[(((((triple11 triple8) -> rule3)) -> rule5))] The cow visits the cow.[(((((triple11 triple8) -> rule3)) -> rule6))]
The cow sees the dog.
("cow" "sees" "dog" "+")
triple1
The dog does not see the cow.
("dog" "sees" "cow" "-")
triple4
The dog is blue.
("dog" "is" "blue" "+")
triple2
The dog is young.
("dog" "is" "young" "+")
triple3
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple5
The tiger eats the dog.
("tiger" "eats" "dog" "+")
triple6
The tiger is blue.
("tiger" "is" "blue" "+")
triple7
The tiger is cold.
("tiger" "is" "cold" "+")
triple8
The tiger is round.
("tiger" "is" "round" "+")
triple9
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple10
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple11
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple12
The cow eats the tiger.
("cow" "eats" "tiger" "+")
((triple11 triple8) -> (rule3 % int1))
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
((triple10) -> (rule2 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow eats the dog.
("cow" "eats" "dog" "+")
((((triple11 triple8) -> (rule3 % int2))) -> (rule5 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
((((triple11 triple8) -> (rule3 % int2))) -> (rule6 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int2