The mouse is red. The mouse is rough. The mouse does not like the tiger. The mouse does not see the tiger. The mouse visits the tiger. The tiger is cold. The tiger is red. The tiger is not rough. The tiger is round. The tiger likes the mouse. The tiger sees the mouse. The tiger visits the mouse. If someone sees the mouse then they are red. If someone is rough and they visit the mouse then the mouse is nice. If someone is rough then they visit the mouse. If someone is nice then they are not round. If someone visits the tiger then the tiger sees the mouse. If someone is nice then they see the mouse. If someone is red then they visit the tiger. If someone is red and not round then they are not cold.
The mouse is red.
("mouse" "is" "red" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse does not like the tiger.
("mouse" "likes" "tiger" "-")
The mouse does not see the tiger.
("mouse" "sees" "tiger" "-")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is not rough.
("tiger" "is" "rough" "-")
The tiger is round.
("tiger" "is" "round" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If someone sees the mouse then they are red.
((("someone" "sees" "mouse" "+")) -> ("someone" "is" "red" "+"))
If someone is rough and they visit the mouse then the mouse is nice.
((("someone" "is" "rough" "+") ("someone" "visits" "mouse" "+")) -> ("mouse" "is" "nice" "+"))
If someone is rough then they visit the mouse.
((("someone" "is" "rough" "+")) -> ("someone" "visits" "mouse" "+"))
If someone is nice then they are not round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "-"))
If someone visits the tiger then the tiger sees the mouse.
((("someone" "visits" "tiger" "+")) -> ("tiger" "sees" "mouse" "+"))
If someone is nice then they see the mouse.
((("someone" "is" "nice" "+")) -> ("someone" "sees" "mouse" "+"))
If someone is red then they visit the tiger.
((("someone" "is" "red" "+")) -> ("someone" "visits" "tiger" "+"))
If someone is red and not round then they are not cold.
((("someone" "is" "red" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "cold" "-"))
The tiger sees the mouse.
True
1
proof
[(triple11 OR ((triple5) -> rule5) OR ((((triple1) -> rule7)) -> rule5) OR ((((triple7) -> rule7)) -> rule5) OR ((((((((((triple2 ((triple2) -> rule3)) -> rule2)) -> rule6)) -> rule1)) -> rule7)) -> rule5))]
("tiger" "sees" "mouse" "+")
triple11
((triple5) -> (rule5 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2
((((triple7) -> (rule7 % int2))) -> (rule5 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
((((((((((triple2 ((triple2) -> (rule3 % int6))) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int4
The mouse is nice.
("mouse" "is" "nice" "+")
int5
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int6
The mouse is not red.
False
1
inv-proof
[(triple1 OR ((((((triple2 ((triple2) -> rule3)) -> rule2)) -> rule6)) -> rule1))]
("mouse" "is" "red" "-")
triple1
((((((triple2 ((triple2) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int4
The tiger visits the tiger.
True
2
proof
[(((triple7) -> rule7) OR ((((triple11) -> rule1)) -> rule7) OR ((((((triple5) -> rule5)) -> rule1)) -> rule7) OR ((((((((triple1) -> rule7)) -> rule5)) -> rule1)) -> rule7) OR ((((((((((((((triple2 ((triple2) -> rule3)) -> rule2)) -> rule6)) -> rule1)) -> rule7)) -> rule5)) -> rule1)) -> rule7))]
("tiger" "visits" "tiger" "+")
((triple7) -> (rule7 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
((((triple11) -> (rule1 % int2))) -> (rule7 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
((((((triple5) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
((((((((triple1) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int4
((((((((((((((triple2 ((triple2) -> (rule3 % int8))) -> (rule2 % int7))) -> (rule6 % int6))) -> (rule1 % int5))) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int4
The mouse is red.
("mouse" "is" "red" "+")
int5
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int6
The mouse is nice.
("mouse" "is" "nice" "+")
int7
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int8
The mouse does not visit the mouse.
False
2
inv-proof
[(((triple2) -> rule3))]
("mouse" "visits" "mouse" "-")
((triple2) -> (rule3 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is nice.
True
4
proof
[(((triple2 ((triple2) -> rule3)) -> rule2))]
("mouse" "is" "nice" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse is not nice.
False
4
inv-proof
[(((triple2 ((triple2) -> rule3)) -> rule2))]
("mouse" "is" "nice" "-")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The tiger is not nice.
Unknown
inv-random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
@0: The mouse does not like the tiger.[(triple3)] The mouse does not see the tiger.[(triple4)] The mouse is red.[(triple1 OR ((((((triple2 ((triple2) -> rule3)) -> rule2)) -> rule6)) -> rule1))] The mouse is rough.[(triple2)] The mouse visits the tiger.[(triple5 OR ((triple1) -> rule7) OR ((((((((triple2 ((triple2) -> rule3)) -> rule2)) -> rule6)) -> rule1)) -> rule7))] The tiger is cold.[(triple6)] The tiger is not rough.[(triple8)] The tiger is red.[(triple7 OR ((triple11) -> rule1) OR ((((triple5) -> rule5)) -> rule1) OR ((((((triple1) -> rule7)) -> rule5)) -> rule1) OR ((((((((((((triple2 ((triple2) -> rule3)) -> rule2)) -> rule6)) -> rule1)) -> rule7)) -> rule5)) -> rule1))] The tiger is round.[(triple9)] The tiger likes the mouse.[(triple10)] The tiger sees the mouse.[(triple11 OR ((triple5) -> rule5) OR ((((triple1) -> rule7)) -> rule5) OR ((((triple7) -> rule7)) -> rule5) OR ((((((((((triple2 ((triple2) -> rule3)) -> rule2)) -> rule6)) -> rule1)) -> rule7)) -> rule5))] The tiger visits the mouse.[(triple12)] @1: The mouse visits the mouse.[(((triple2) -> rule3))] The tiger visits the tiger.[(((triple7) -> rule7) OR ((((triple11) -> rule1)) -> rule7) OR ((((((triple5) -> rule5)) -> rule1)) -> rule7) OR ((((((((triple1) -> rule7)) -> rule5)) -> rule1)) -> rule7) OR ((((((((((((((triple2 ((triple2) -> rule3)) -> rule2)) -> rule6)) -> rule1)) -> rule7)) -> rule5)) -> rule1)) -> rule7))] @2: The mouse is nice.[(((triple2 ((triple2) -> rule3)) -> rule2))] @3: The mouse is not round.[(((((triple2 ((triple2) -> rule3)) -> rule2)) -> rule4))] The mouse sees the mouse.[(((((triple2 ((triple2) -> rule3)) -> rule2)) -> rule6))] @4: The mouse is not cold.[(((triple1 ((((triple2 ((triple2) -> rule3)) -> rule2)) -> rule4)) -> rule8) OR ((((((((triple2 ((triple2) -> rule3)) -> rule2)) -> rule6)) -> rule1) ((((triple2 ((triple2) -> rule3)) -> rule2)) -> rule4)) -> rule8))]
The mouse does not like the tiger.
("mouse" "likes" "tiger" "-")
triple3
The mouse does not see the tiger.
("mouse" "sees" "tiger" "-")
triple4
The mouse is red.
("mouse" "is" "red" "+")
triple1
((((((triple2 ((triple2) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int4
The mouse is rough.
("mouse" "is" "rough" "+")
triple2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple5
((triple1) -> (rule7 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
((((((((triple2 ((triple2) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int3
The mouse is nice.
("mouse" "is" "nice" "+")
int4
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int5
The tiger is cold.
("tiger" "is" "cold" "+")
triple6
The tiger is not rough.
("tiger" "is" "rough" "-")
triple8
The tiger is red.
("tiger" "is" "red" "+")
triple7
((triple11) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
((((triple5) -> (rule5 % int2))) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
((((((triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int3
((((((((((((triple2 ((triple2) -> (rule3 % int7))) -> (rule2 % int6))) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int3
The mouse is red.
("mouse" "is" "red" "+")
int4
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int5
The mouse is nice.
("mouse" "is" "nice" "+")
int6
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int7
The tiger is round.
("tiger" "is" "round" "+")
triple9
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple10
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple11
((triple5) -> (rule5 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2
((((triple7) -> (rule7 % int2))) -> (rule5 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
((((((((((triple2 ((triple2) -> (rule3 % int6))) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int4
The mouse is nice.
("mouse" "is" "nice" "+")
int5
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int6
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple12
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((triple2) -> (rule3 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple7) -> (rule7 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
((((triple11) -> (rule1 % int2))) -> (rule7 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
((((((triple5) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
((((((((triple1) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int4
((((((((((((((triple2 ((triple2) -> (rule3 % int8))) -> (rule2 % int7))) -> (rule6 % int6))) -> (rule1 % int5))) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int4
The mouse is red.
("mouse" "is" "red" "+")
int5
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int6
The mouse is nice.
("mouse" "is" "nice" "+")
int7
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int8
The mouse is nice.
("mouse" "is" "nice" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse is not round.
("mouse" "is" "round" "-")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int3
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int3
The mouse is not cold.
("mouse" "is" "cold" "-")
((triple1 ((((triple2 ((triple2) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The mouse is not cold.
("mouse" "is" "cold" "-")
int1
The mouse is not round.
("mouse" "is" "round" "-")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int4
((((((((triple2 ((triple2) -> (rule3 % int6))) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule1 % int3)) ((((triple2 ((triple2) -> (rule3 % int6))) -> (rule2 % int5))) -> (rule4 % int2))) -> (rule8 % int1))
The mouse is not cold.
("mouse" "is" "cold" "-")
int1
The mouse is not round.
("mouse" "is" "round" "-")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int4
The mouse is nice.
("mouse" "is" "nice" "+")
int5
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int6