The mouse chases the tiger. The mouse is big. The mouse is cold. The mouse is kind. The mouse is nice. The mouse is round. The mouse needs the tiger. The mouse visits the tiger. The tiger chases the mouse. The tiger is big. The tiger is cold. The tiger is kind. The tiger is nice. The tiger is round. The tiger needs the mouse. The tiger visits the mouse. If the mouse visits the tiger and the mouse is kind then the mouse needs the tiger. If something needs the tiger and the tiger chases the mouse then the tiger is cold. If something needs the mouse and it is cold then the mouse is cold. If something needs the mouse and the mouse is round then it chases the tiger. All nice things are cold. If the mouse chases the tiger and the tiger chases the mouse then the mouse is cold. All big things are kind. If something needs the tiger then it chases the tiger.
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If the mouse visits the tiger and the mouse is kind then the mouse needs the tiger.
((("mouse" "visits" "tiger" "+") ("mouse" "is" "kind" "+")) -> ("mouse" "needs" "tiger" "+"))
If something needs the tiger and the tiger chases the mouse then the tiger is cold.
((("something" "needs" "tiger" "+") ("tiger" "chases" "mouse" "+")) -> ("tiger" "is" "cold" "+"))
If something needs the mouse and it is cold then the mouse is cold.
((("something" "needs" "mouse" "+") ("something" "is" "cold" "+")) -> ("mouse" "is" "cold" "+"))
If something needs the mouse and the mouse is round then it chases the tiger.
((("something" "needs" "mouse" "+") ("mouse" "is" "round" "+")) -> ("something" "chases" "tiger" "+"))
All nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If the mouse chases the tiger and the tiger chases the mouse then the mouse is cold.
((("mouse" "chases" "tiger" "+") ("tiger" "chases" "mouse" "+")) -> ("mouse" "is" "cold" "+"))
All big things are kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something needs the tiger then it chases the tiger.
((("something" "needs" "tiger" "+")) -> ("something" "chases" "tiger" "+"))
The tiger is kind.
True
1
proof
[(triple12 OR ((triple10) -> rule7))]
("tiger" "is" "kind" "+")
triple12
((triple10) -> (rule7 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The mouse is not big.
False
1
inv-proof
[(triple2)]
("mouse" "is" "big" "-")
triple2
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 tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
@0: The mouse chases the tiger.[(triple1 OR ((triple7) -> rule8) OR ((((triple8 triple4) -> rule1)) -> rule8) OR ((((triple8 ((triple2) -> rule7)) -> rule1)) -> rule8))] The mouse is big.[(triple2)] The mouse is cold.[(triple3 OR ((triple5) -> rule5) OR ((triple1 triple9) -> rule6) OR ((triple15 triple11) -> rule3) OR ((triple15 ((triple13) -> rule5)) -> rule3) OR ((triple15 ((triple7 triple9) -> rule2)) -> rule3) OR ((((triple7) -> rule8) triple9) -> rule6) OR ((triple15 ((((triple8 triple4) -> rule1) triple9) -> rule2)) -> rule3) OR ((((((triple8 triple4) -> rule1)) -> rule8) triple9) -> rule6) OR ((triple15 ((((triple8 ((triple2) -> rule7)) -> rule1) triple9) -> rule2)) -> rule3) OR ((((((triple8 ((triple2) -> rule7)) -> rule1)) -> rule8) triple9) -> rule6))] The mouse is kind.[(triple4 OR ((triple2) -> rule7))] The mouse is nice.[(triple5)] The mouse is round.[(triple6)] The mouse needs the tiger.[(triple7 OR ((triple8 triple4) -> rule1) OR ((triple8 ((triple2) -> rule7)) -> rule1))] The mouse visits the tiger.[(triple8)] The tiger chases the mouse.[(triple9)] The tiger is big.[(triple10)] The tiger is cold.[(triple11 OR ((triple13) -> rule5) OR ((triple7 triple9) -> rule2) OR ((((triple8 triple4) -> rule1) triple9) -> rule2) OR ((((triple8 ((triple2) -> rule7)) -> rule1) triple9) -> rule2))] The tiger is kind.[(triple12 OR ((triple10) -> rule7))] The tiger is nice.[(triple13)] The tiger is round.[(triple14)] The tiger needs the mouse.[(triple15)] The tiger visits the mouse.[(triple16)] @1: The tiger chases the tiger.[(((triple15 triple6) -> rule4))]
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple1
((triple7) -> (rule8 % int1))
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int1
((((triple8 triple4) -> (rule1 % int2))) -> (rule8 % int1))
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int1
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int2
((((triple8 ((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int1
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The mouse is big.
("mouse" "is" "big" "+")
triple2
The mouse is cold.
("mouse" "is" "cold" "+")
triple3
((triple5) -> (rule5 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
((triple1 triple9) -> (rule6 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
((triple15 triple11) -> (rule3 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
((triple15 ((triple13) -> (rule5 % int2))) -> (rule3 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
((triple15 ((triple7 triple9) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
((((triple7) -> (rule8 % int2)) triple9) -> (rule6 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int2
((triple15 ((((triple8 triple4) -> (rule1 % int3)) triple9) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int3
((((((triple8 triple4) -> (rule1 % int3))) -> (rule8 % int2)) triple9) -> (rule6 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int2
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int3
((triple15 ((((triple8 ((triple2) -> (rule7 % int4))) -> (rule1 % int3)) triple9) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
int4
((((((triple8 ((triple2) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule8 % int2)) triple9) -> (rule6 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int2
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
int4
The mouse is kind.
("mouse" "is" "kind" "+")
triple4
((triple2) -> (rule7 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
triple5
The mouse is round.
("mouse" "is" "round" "+")
triple6
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple7
((triple8 triple4) -> (rule1 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
((triple8 ((triple2) -> (rule7 % int2))) -> (rule1 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple8
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple9
The tiger is big.
("tiger" "is" "big" "+")
triple10
The tiger is cold.
("tiger" "is" "cold" "+")
triple11
((triple13) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
((triple7 triple9) -> (rule2 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
((((triple8 triple4) -> (rule1 % int2)) triple9) -> (rule2 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int2
((((triple8 ((triple2) -> (rule7 % int3))) -> (rule1 % int2)) triple9) -> (rule2 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The tiger is kind.
("tiger" "is" "kind" "+")
triple12
((triple10) -> (rule7 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
triple13
The tiger is round.
("tiger" "is" "round" "+")
triple14
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple15
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple16
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((triple15 triple6) -> (rule4 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1