Harry is blue. White people are quiet. If someone is cold and not blue then they are quiet. All blue people are not red. If someone is quiet and not blue then they are not cold. Blue people are white. If Harry is white and Harry is quiet then Harry is cold. If someone is white and not blue then they are furry. If someone is quiet and not white then they are not rough.
Harry is blue.
("Harry" "is" "blue" "+")
White people are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If someone is cold and not blue then they are quiet.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "quiet" "+"))
All blue people are not red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "-"))
If someone is quiet and not blue then they are not cold.
((("someone" "is" "quiet" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "cold" "-"))
Blue people are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
If Harry is white and Harry is quiet then Harry is cold.
((("Harry" "is" "white" "+") ("Harry" "is" "quiet" "+")) -> ("Harry" "is" "cold" "+"))
If someone is white and not blue then they are furry.
((("someone" "is" "white" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "furry" "+"))
If someone is quiet and not white then they are not rough.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "~")) -> ("someone" "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 white.
True
2
proof
[(((triple1) -> rule5))]
("Harry" "is" "white" "+")
((triple1) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple1) -> rule5))]
("Harry" "is" "white" "-")
((triple1) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is quiet.
True
3
proof
[(((((triple1) -> rule5)) -> rule1))]
("Harry" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not quiet.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule1))]
("Harry" "is" "quiet" "-")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is cold.
True
6
proof
[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule1)) -> rule6))]
("Harry" "is" "cold" "+")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is not cold.
False
6
inv-proof
[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule1)) -> rule6))]
("Harry" "is" "cold" "-")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is not furry.
Unknown
inv-rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "furry" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Harry is blue.[(triple1)] @1: Harry is not red.[(((triple1) -> rule3))] Harry is white.[(((triple1) -> rule5))] @2: Harry is quiet.[(((((triple1) -> rule5)) -> rule1))] @3: Harry is cold.[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule1)) -> rule6))]
Harry is blue.
("Harry" "is" "blue" "+")
triple1
Harry is not red.
("Harry" "is" "red" "-")
((triple1) -> (rule3 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple1) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3