Gary is rough. Harry is rough. If Gary is kind and Gary is blue then Gary is not white. If something is green then it is blue. Rough things are kind. If something is smart then it is white. If something is kind and green then it is red. If something is blue then it is rough. If something is rough then it is green. If Harry is kind and Harry is not green then Harry is white.
Gary is rough.
("Gary" "is" "rough" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If Gary is kind and Gary is blue then Gary is not white.
((("Gary" "is" "kind" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "white" "-"))
If something is green then it is blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
Rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If something is smart then it is white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If something is kind and green then it is red.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If something is blue then it is rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If something is rough then it is green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
If Harry is kind and Harry is not green then Harry is white.
((("Harry" "is" "kind" "+") ("Harry" "is" "green" "~")) -> ("Harry" "is" "white" "+"))
Harry is rough.
True
1
proof
[(triple2)]
("Harry" "is" "rough" "+")
triple2
Harry is not rough.
False
1
inv-proof
[(triple2)]
("Harry" "is" "rough" "-")
triple2
Harry is green.
True
2
proof
[(((triple2) -> rule7))]
("Harry" "is" "green" "+")
((triple2) -> (rule7 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not kind.
False
2
inv-proof
[(((triple2) -> rule3))]
("Harry" "is" "kind" "-")
((triple2) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Gary is red.
True
5
proof
[(((((triple1) -> rule3) ((triple1) -> rule7)) -> rule5))]
("Gary" "is" "red" "+")
((((triple1) -> (rule3 % int3)) ((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is not red.
False
5
inv-proof
[(((((triple1) -> rule3) ((triple1) -> rule7)) -> rule5))]
("Gary" "is" "red" "-")
((((triple1) -> (rule3 % int3)) ((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is not white.
True
6
proof
[(((((triple1) -> rule3) ((((triple1) -> rule7)) -> rule2)) -> rule1))]
("Gary" "is" "white" "-")
((((triple1) -> (rule3 % int4)) ((((triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
Gary is white.
False
6
inv-proof
[(((((triple1) -> rule3) ((((triple1) -> rule7)) -> rule2)) -> rule1))]
("Gary" "is" "white" "+")
((((triple1) -> (rule3 % int4)) ((((triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
Harry is not white.
Unknown
inv-rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "white" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Gary is rough.[(triple1)] Harry is rough.[(triple2)] @1: Gary is green.[(((triple1) -> rule7))] Gary is kind.[(((triple1) -> rule3))] Harry is green.[(((triple2) -> rule7))] Harry is kind.[(((triple2) -> rule3))] @2: Gary is blue.[(((((triple1) -> rule7)) -> rule2))] Gary is red.[(((((triple1) -> rule3) ((triple1) -> rule7)) -> rule5))] Harry is blue.[(((((triple2) -> rule7)) -> rule2))] Harry is red.[(((((triple2) -> rule3) ((triple2) -> rule7)) -> rule5))] @3: Gary is not white.[(((((triple1) -> rule3) ((((triple1) -> rule7)) -> rule2)) -> rule1))]
Gary is rough.
("Gary" "is" "rough" "+")
triple1
Harry is rough.
("Harry" "is" "rough" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
((triple1) -> (rule7 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple2) -> (rule7 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((((triple1) -> (rule7 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((((triple1) -> (rule3 % int3)) ((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
((((triple2) -> (rule7 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((((triple2) -> (rule3 % int3)) ((triple2) -> (rule7 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Gary is not white.
("Gary" "is" "white" "-")
((((triple1) -> (rule3 % int4)) ((((triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4