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