Harry is cold. Harry is furry. Harry is white. White things are big. All rough things are nice. Blue, cold things are big. If Harry is big and Harry is cold then Harry is nice. Cold, rough things are white. All cold things are furry.
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is white.
("Harry" "is" "white" "+")
White things are big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
All rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
Blue, cold things are big.
((("something" "is" "blue" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If Harry is big and Harry is cold then Harry is nice.
((("Harry" "is" "big" "+") ("Harry" "is" "cold" "+")) -> ("Harry" "is" "nice" "+"))
Cold, rough things are white.
((("something" "is" "cold" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
All cold things are furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
Harry is white.
True
1
proof
[(triple3)]
("Harry" "is" "white" "+")
triple3
Harry is not white.
False
1
inv-proof
[(triple3)]
("Harry" "is" "white" "-")
triple3
Harry is big.
True
2
proof
[(((triple3) -> rule1))]
("Harry" "is" "big" "+")
((triple3) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple3) -> rule1))]
("Harry" "is" "big" "-")
((triple3) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
True
4
proof
[(((((triple3) -> rule1) triple1) -> rule4))]
("Harry" "is" "nice" "+")
((((triple3) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not nice.
False
4
inv-proof
[(((((triple3) -> rule1) triple1) -> rule4))]
("Harry" "is" "nice" "-")
((((triple3) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Harry is cold.[(triple1)] Harry is furry.[(triple2 OR ((triple1) -> rule6))] Harry is white.[(triple3)] @1: Harry is big.[(((triple3) -> rule1))] @2: Harry is nice.[(((((triple3) -> rule1) triple1) -> rule4))]
Harry is cold.
("Harry" "is" "cold" "+")
triple1
Harry is furry.
("Harry" "is" "furry" "+")
triple2
((triple1) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
((triple3) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((((triple3) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2