The bald eagle likes the cow. The cow is nice. The tiger likes the cow. If something likes the tiger then it is red. If something likes the cow then the cow likes the tiger. If something is red and it likes the tiger then it does not visit the tiger. If something is round then it visits the cow. If something is blue then it eats the bald eagle. If the cow likes the bald eagle and the cow does not like the tiger then the bald eagle does not visit the cow.
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
The cow is nice.
("cow" "is" "nice" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
If something likes the tiger then it is red.
((("something" "likes" "tiger" "+")) -> ("something" "is" "red" "+"))
If something likes the cow then the cow likes the tiger.
((("something" "likes" "cow" "+")) -> ("cow" "likes" "tiger" "+"))
If something is red and it likes the tiger then it does not visit the tiger.
((("something" "is" "red" "+") ("something" "likes" "tiger" "+")) -> ("something" "visits" "tiger" "-"))
If something is round then it visits the cow.
((("something" "is" "round" "+")) -> ("something" "visits" "cow" "+"))
If something is blue then it eats the bald eagle.
((("something" "is" "blue" "+")) -> ("something" "eats" "bald eagle" "+"))
If the cow likes the bald eagle and the cow does not like the tiger then the bald eagle does not visit the cow.
((("cow" "likes" "bald eagle" "+") ("cow" "likes" "tiger" "~")) -> ("bald eagle" "visits" "cow" "-"))
The bald eagle likes the cow.
True
1
proof
[(triple1)]
("bald eagle" "likes" "cow" "+")
triple1
The bald eagle does not like the cow.
False
1
inv-proof
[(triple1)]
("bald eagle" "likes" "cow" "-")
triple1
The cow likes the tiger.
True
2
proof
[(((triple1) -> rule2) OR ((triple3) -> rule2))]
("cow" "likes" "tiger" "+")
((triple1) -> (rule2 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
((triple3) -> (rule2 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The cow does not like the tiger.
False
2
inv-proof
[(((triple1) -> rule2) OR ((triple3) -> rule2))]
("cow" "likes" "tiger" "-")
((triple1) -> (rule2 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
((triple3) -> (rule2 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The cow is red.
True
3
proof
[(((((triple1) -> rule2)) -> rule1) OR ((((triple3) -> rule2)) -> rule1))]
("cow" "is" "red" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int2
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int2
The cow is not red.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1) OR ((((triple3) -> rule2)) -> rule1))]
("cow" "is" "red" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int2
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int2
The cow does not visit the tiger.
True
6
proof
[(((((((triple1) -> rule2)) -> rule1) ((triple1) -> rule2)) -> rule3) OR ((((((triple1) -> rule2)) -> rule1) ((triple3) -> rule2)) -> rule3) OR ((((((triple3) -> rule2)) -> rule1) ((triple1) -> rule2)) -> rule3) OR ((((((triple3) -> rule2)) -> rule1) ((triple3) -> rule2)) -> rule3))]
("cow" "visits" "tiger" "-")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2)) ((triple1) -> (rule2 % int3))) -> (rule3 % int1))
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int3
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2)) ((triple3) -> (rule2 % int3))) -> (rule3 % int1))
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int3
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2)) ((triple1) -> (rule2 % int3))) -> (rule3 % int1))
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int3
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2)) ((triple3) -> (rule2 % int3))) -> (rule3 % int1))
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int3
The cow visits the tiger.
False
6
inv-proof
[(((((((triple1) -> rule2)) -> rule1) ((triple1) -> rule2)) -> rule3) OR ((((((triple1) -> rule2)) -> rule1) ((triple3) -> rule2)) -> rule3) OR ((((((triple3) -> rule2)) -> rule1) ((triple1) -> rule2)) -> rule3) OR ((((((triple3) -> rule2)) -> rule1) ((triple3) -> rule2)) -> rule3))]
("cow" "visits" "tiger" "+")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2)) ((triple1) -> (rule2 % int3))) -> (rule3 % int1))
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int3
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2)) ((triple3) -> (rule2 % int3))) -> (rule3 % int1))
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int3
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2)) ((triple1) -> (rule2 % int3))) -> (rule3 % int1))
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int3
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2)) ((triple3) -> (rule2 % int3))) -> (rule3 % int1))
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int3
The cow does not visit the cow.
Unknown
inv-rconc
[@1: The cow visits the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "visits" "cow" "-")
The tiger visits the cow.
Unknown
rconc
[@1: The tiger visits the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "visits" "cow" "+")
The tiger is not red.
Unknown
inv-rconc
[@1: The tiger is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "red" "-")
The cow eats the bald eagle.
Unknown
rconc
[@1: The cow eats the bald eagle.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "eats" "bald eagle" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The bald eagle eats the cow.
Unknown
random
[@0: The bald eagle eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "eats" "cow" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The cow eats the tiger.
Unknown
random
[@0: The cow eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "tiger" "+")
@0: The bald eagle likes the cow.[(triple1)] The cow is nice.[(triple2)] The tiger likes the cow.[(triple3)] @1: The cow likes the tiger.[(((triple1) -> rule2) OR ((triple3) -> rule2))] @2: The cow is red.[(((((triple1) -> rule2)) -> rule1) OR ((((triple3) -> rule2)) -> rule1))] @3: The cow does not visit the tiger.[(((((((triple1) -> rule2)) -> rule1) ((triple1) -> rule2)) -> rule3) OR ((((((triple1) -> rule2)) -> rule1) ((triple3) -> rule2)) -> rule3) OR ((((((triple3) -> rule2)) -> rule1) ((triple1) -> rule2)) -> rule3) OR ((((((triple3) -> rule2)) -> rule1) ((triple3) -> rule2)) -> rule3))]
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
triple2
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple3
The cow likes the tiger.
("cow" "likes" "tiger" "+")
((triple1) -> (rule2 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
((triple3) -> (rule2 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The cow is red.
("cow" "is" "red" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int2
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int2
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2)) ((triple1) -> (rule2 % int3))) -> (rule3 % int1))
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int3
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2)) ((triple3) -> (rule2 % int3))) -> (rule3 % int1))
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int3
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2)) ((triple1) -> (rule2 % int3))) -> (rule3 % int1))
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int3
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2)) ((triple3) -> (rule2 % int3))) -> (rule3 % int1))
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int3