The bald eagle likes the mouse. The bald eagle sees the tiger. The cow is green. The cow sees the bald eagle. The cow sees the tiger. The cow visits the mouse. The mouse is green. The mouse likes the cow. The tiger is cold. The tiger visits the cow. If something likes the tiger then it likes the mouse. If something visits the bald eagle then the bald eagle sees the mouse. If something likes the cow then the cow visits the tiger. If the bald eagle sees the mouse then the mouse likes the tiger. If the bald eagle visits the cow and the bald eagle is cold then the bald eagle sees the tiger. If the cow visits the tiger then the cow visits the bald eagle.
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
The cow is green.
("cow" "is" "green" "+")
The cow sees the bald eagle.
("cow" "sees" "bald eagle" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If something likes the tiger then it likes the mouse.
((("something" "likes" "tiger" "+")) -> ("something" "likes" "mouse" "+"))
If something visits the bald eagle then the bald eagle sees the mouse.
((("something" "visits" "bald eagle" "+")) -> ("bald eagle" "sees" "mouse" "+"))
If something likes the cow then the cow visits the tiger.
((("something" "likes" "cow" "+")) -> ("cow" "visits" "tiger" "+"))
If the bald eagle sees the mouse then the mouse likes the tiger.
((("bald eagle" "sees" "mouse" "+")) -> ("mouse" "likes" "tiger" "+"))
If the bald eagle visits the cow and the bald eagle is cold then the bald eagle sees the tiger.
((("bald eagle" "visits" "cow" "+") ("bald eagle" "is" "cold" "+")) -> ("bald eagle" "sees" "tiger" "+"))
If the cow visits the tiger then the cow visits the bald eagle.
((("cow" "visits" "tiger" "+")) -> ("cow" "visits" "bald eagle" "+"))
The mouse likes the cow.
True
1
proof
[(triple8)]
("mouse" "likes" "cow" "+")
triple8
The mouse does not like the cow.
False
1
inv-proof
[(triple8)]
("mouse" "likes" "cow" "-")
triple8
The cow visits the tiger.
True
2
proof
[(((triple8) -> rule3))]
("cow" "visits" "tiger" "+")
((triple8) -> (rule3 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The cow does not visit the tiger.
False
2
inv-proof
[(((triple8) -> rule3))]
("cow" "visits" "tiger" "-")
((triple8) -> (rule3 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The cow visits the bald eagle.
True
3
proof
[(((((triple8) -> rule3)) -> rule6))]
("cow" "visits" "bald eagle" "+")
((((triple8) -> (rule3 % int2))) -> (rule6 % int1))
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
int1
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int2
The cow does not visit the bald eagle.
False
3
inv-proof
[(((((triple8) -> rule3)) -> rule6))]
("cow" "visits" "bald eagle" "-")
((((triple8) -> (rule3 % int2))) -> (rule6 % int1))
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
int1
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int2
The bald eagle sees the mouse.
True
4
proof
[(((((((triple8) -> rule3)) -> rule6)) -> rule2))]
("bald eagle" "sees" "mouse" "+")
((((((triple8) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int1
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
int2
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int3
The bald eagle does not see the mouse.
False
4
inv-proof
[(((((((triple8) -> rule3)) -> rule6)) -> rule2))]
("bald eagle" "sees" "mouse" "-")
((((((triple8) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int1
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
int2
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int3
The mouse likes the tiger.
True
5
proof
[(((((((((triple8) -> rule3)) -> rule6)) -> rule2)) -> rule4))]
("mouse" "likes" "tiger" "+")
((((((((triple8) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int2
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
int3
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int4
The mouse does not like the tiger.
False
5
inv-proof
[(((((((((triple8) -> rule3)) -> rule6)) -> rule2)) -> rule4))]
("mouse" "likes" "tiger" "-")
((((((((triple8) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int2
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
int3
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int4
The mouse likes the mouse.
True
6
proof
[(((((((((((triple8) -> rule3)) -> rule6)) -> rule2)) -> rule4)) -> rule1))]
("mouse" "likes" "mouse" "+")
((((((((((triple8) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int3
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
int4
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int5
The mouse does not like the mouse.
False
6
inv-proof
[(((((((((((triple8) -> rule3)) -> rule6)) -> rule2)) -> rule4)) -> rule1))]
("mouse" "likes" "mouse" "-")
((((((((((triple8) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int3
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
int4
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int5
The tiger does not like the mouse.
Unknown
inv-rconc
[@1: The tiger likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "likes" "mouse" "-")
The cow likes the mouse.
Unknown
rconc
[@1: The cow likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "likes" "mouse" "+")
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 bald eagle likes the tiger.
Unknown
random
[@0: The bald eagle likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "likes" "tiger" "+")
The mouse is not red.
Unknown
inv-random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "-")
The bald eagle is green.
Unknown
random
[@0: The bald eagle is green.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "green" "+")
The cow is not cold.
Unknown
inv-random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
The mouse does not see the bald eagle.
Unknown
inv-random
[@0: The mouse sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "bald eagle" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The cow does not like the tiger.
Unknown
inv-random
[@0: The cow likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "tiger" "-")
The mouse visits the bald eagle.
Unknown
random
[@0: The mouse visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "bald eagle" "+")
@0: The bald eagle likes the mouse.[(triple1)] The bald eagle sees the tiger.[(triple2)] The cow is green.[(triple3)] The cow sees the bald eagle.[(triple4)] The cow sees the tiger.[(triple5)] The cow visits the mouse.[(triple6)] The mouse is green.[(triple7)] The mouse likes the cow.[(triple8)] The tiger is cold.[(triple9)] The tiger visits the cow.[(triple10)] @1: The cow visits the tiger.[(((triple8) -> rule3))] @2: The cow visits the bald eagle.[(((((triple8) -> rule3)) -> rule6))] @3: The bald eagle sees the mouse.[(((((((triple8) -> rule3)) -> rule6)) -> rule2))] @4: The mouse likes the tiger.[(((((((((triple8) -> rule3)) -> rule6)) -> rule2)) -> rule4))] @5: The mouse likes the mouse.[(((((((((((triple8) -> rule3)) -> rule6)) -> rule2)) -> rule4)) -> rule1))]
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
triple1
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
triple2
The cow is green.
("cow" "is" "green" "+")
triple3
The cow sees the bald eagle.
("cow" "sees" "bald eagle" "+")
triple4
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple5
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple6
The mouse is green.
("mouse" "is" "green" "+")
triple7
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple8
The tiger is cold.
("tiger" "is" "cold" "+")
triple9
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple10
The cow visits the tiger.
("cow" "visits" "tiger" "+")
((triple8) -> (rule3 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
((((triple8) -> (rule3 % int2))) -> (rule6 % int1))
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
int1
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int2
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
((((((triple8) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int1
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
int2
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int3
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
((((((((triple8) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int2
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
int3
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int4
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((((((((((triple8) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int3
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
int4
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int5