Harry is blue. If something is red then it is green. If Harry is big then Harry is green. All blue things are red. If something is green then it is big. If something is big and not green then it is not rough. All big, blue things are rough.
Harry is blue.
("Harry" "is" "blue" "+")
If something is red then it is green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If Harry is big then Harry is green.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "green" "+"))
All blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
If something is green then it is big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If something is big and not green then it is not rough.
((("something" "is" "big" "+") ("something" "is" "green" "~")) -> ("something" "is" "rough" "-"))
All big, blue things are rough.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
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 red.
True
2
proof
[(((triple1) -> rule3))]
("Harry" "is" "red" "+")
((triple1) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is not red.
False
2
inv-proof
[(((triple1) -> rule3))]
("Harry" "is" "red" "-")
((triple1) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Harry" "is" "green" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not green.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Harry" "is" "green" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is big.
True
4
proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule4))]
("Harry" "is" "big" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is not big.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule4))]
("Harry" "is" "big" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Harry is blue.[(triple1)] @1: Harry is red.[(((triple1) -> rule3))] @2: Harry is green.[(((((triple1) -> rule3)) -> rule1))] @3: Harry is big.[(((((((triple1) -> rule3)) -> rule1)) -> rule4))] @4: Harry is rough.[(((((((((triple1) -> rule3)) -> rule1)) -> rule4) triple1) -> rule6))]
Harry is blue.
("Harry" "is" "blue" "+")
triple1
Harry is red.
("Harry" "is" "red" "+")
((triple1) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
((((((((triple1) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4