Anne is red. Dave is smart. Gary is rough. Harry is red. If Gary is white then Gary is smart. White, smart things are red. If Gary is rough then Gary is white. All white, furry things are nice. If something is blue and not rough then it is nice. If something is nice and not smart then it is blue.
Anne is red.
("Anne" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is red.
("Harry" "is" "red" "+")
If Gary is white then Gary is smart.
((("Gary" "is" "white" "+")) -> ("Gary" "is" "smart" "+"))
White, smart things are red.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
If Gary is rough then Gary is white.
((("Gary" "is" "rough" "+")) -> ("Gary" "is" "white" "+"))
All white, furry things are nice.
((("something" "is" "white" "+") ("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If something is blue and not rough then it is nice.
((("something" "is" "blue" "+") ("something" "is" "rough" "~")) -> ("something" "is" "nice" "+"))
If something is nice and not smart then it is blue.
((("something" "is" "nice" "+") ("something" "is" "smart" "~")) -> ("something" "is" "blue" "+"))
Harry is red.
True
1
proof
[(triple4)]
("Harry" "is" "red" "+")
triple4
Dave is not smart.
False
1
inv-proof
[(triple2)]
("Dave" "is" "smart" "-")
triple2
Gary is white.
True
2
proof
[(((triple3) -> rule3))]
("Gary" "is" "white" "+")
((triple3) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not white.
False
2
inv-proof
[(((triple3) -> rule3))]
("Gary" "is" "white" "-")
((triple3) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is smart.
True
3
proof
[(((((triple3) -> rule3)) -> rule1))]
("Gary" "is" "smart" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not smart.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule1))]
("Gary" "is" "smart" "-")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is red.
True
6
proof
[(((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule1)) -> rule2))]
("Gary" "is" "red" "+")
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is not red.
False
6
inv-proof
[(((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule1)) -> rule2))]
("Gary" "is" "red" "-")
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "blue" "-")
Gary is nice.
Unknown
rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "nice" "+")
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "blue" "-")
Dave is red.
Unknown
rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "red" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Anne is red.[(triple1)] Dave is smart.[(triple2)] Gary is rough.[(triple3)] Harry is red.[(triple4)] @1: Gary is white.[(((triple3) -> rule3))] @2: Gary is smart.[(((((triple3) -> rule3)) -> rule1))] @3: Gary is red.[(((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule1)) -> rule2))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Gary is rough.
("Gary" "is" "rough" "+")
triple3
Harry is red.
("Harry" "is" "red" "+")
triple4
Gary is white.
("Gary" "is" "white" "+")
((triple3) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3