Harry is blue. If Harry is blue then Harry is big. All big, rough people are cold. If someone is kind and cold then they are round. If Harry is big then Harry is round. Blue, rough people are cold. If Harry is round and Harry is blue then Harry is rough. If someone is rough then they are round. If someone is cold then they are blue.
Harry is blue.
("Harry" "is" "blue" "+")
If Harry is blue then Harry is big.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "big" "+"))
All big, rough people are cold.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If someone is kind and cold then they are round.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If Harry is big then Harry is round.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "round" "+"))
Blue, rough people are cold.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If Harry is round and Harry is blue then Harry is rough.
((("Harry" "is" "round" "+") ("Harry" "is" "blue" "+")) -> ("Harry" "is" "rough" "+"))
If someone is rough then they are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
If someone is cold then they are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
Harry is blue.
True
1
proof
[(triple1)]
("Harry" "is" "blue" "+")
triple1
Harry is not blue.
False
1
inv-proof
[(triple1)]
("Harry" "is" "blue" "-")
triple1
Harry is big.
True
2
proof
[(((triple1) -> rule1))]
("Harry" "is" "big" "+")
((triple1) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple1) -> rule1))]
("Harry" "is" "big" "-")
((triple1) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("Harry" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not round.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule4))]
("Harry" "is" "round" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is rough.
True
5
proof
[(((((((triple1) -> rule1)) -> rule4) triple1) -> rule6))]
("Harry" "is" "rough" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not rough.
False
5
inv-proof
[(((((((triple1) -> rule1)) -> rule4) triple1) -> rule6))]
("Harry" "is" "rough" "-")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Harry is blue.[(triple1)] @1: Harry is big.[(((triple1) -> rule1))] @2: Harry is round.[(((((triple1) -> rule1)) -> rule4))] @3: Harry is rough.[(((((((triple1) -> rule1)) -> rule4) triple1) -> rule6))] @4: Harry is cold.[(((triple1 ((((((triple1) -> rule1)) -> rule4) triple1) -> rule6)) -> rule5) OR ((((triple1) -> rule1) ((((((triple1) -> rule1)) -> rule4) triple1) -> rule6)) -> rule2))]
Harry is blue.
("Harry" "is" "blue" "+")
triple1
Harry is big.
("Harry" "is" "big" "+")
((triple1) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
((triple1 ((((((triple1) -> (rule1 % int4))) -> (rule4 % int3)) triple1) -> (rule6 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
((((triple1) -> (rule1 % int4)) ((((((triple1) -> (rule1 % int4))) -> (rule4 % int3)) triple1) -> (rule6 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4