Gary is cold. Gary is green. Gary is nice. Gary is white. Harry is blue. Harry is green. Harry is white. If Gary is not white then Gary is nice. If something is cold then it is quiet. All white things are cold. All white things are cold. If something is blue and not cold then it is green. If something is green and not blue then it is smart.
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is white.
("Harry" "is" "white" "+")
If Gary is not white then Gary is nice.
((("Gary" "is" "white" "~")) -> ("Gary" "is" "nice" "+"))
If something is cold then it is quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
All white things are cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
All white things are cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If something is blue and not cold then it is green.
((("something" "is" "blue" "+") ("something" "is" "cold" "~")) -> ("something" "is" "green" "+"))
If something is green and not blue then it is smart.
((("something" "is" "green" "+") ("something" "is" "blue" "~")) -> ("something" "is" "smart" "+"))
Gary is green.
True
1
proof
[(triple2)]
("Gary" "is" "green" "+")
triple2
Harry is not blue.
False
1
inv-proof
[(triple5)]
("Harry" "is" "blue" "-")
triple5
Harry is cold.
True
2
proof
[(((triple7) -> rule3) OR ((triple7) -> rule4))]
("Harry" "is" "cold" "+")
((triple7) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple7) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Gary is not quiet.
False
2
inv-proof
[(((triple1) -> rule2) OR ((((triple4) -> rule3)) -> rule2) OR ((((triple4) -> rule4)) -> rule2))]
("Gary" "is" "quiet" "-")
((triple1) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Harry is quiet.
True
3
proof
[(((((triple7) -> rule3)) -> rule2) OR ((((triple7) -> rule4)) -> rule2))]
("Harry" "is" "quiet" "+")
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple7) -> (rule4 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not quiet.
False
3
inv-proof
[(((((triple7) -> rule3)) -> rule2) OR ((((triple7) -> rule4)) -> rule2))]
("Harry" "is" "quiet" "-")
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple7) -> (rule4 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "smart" "-")
Harry is smart.
Unknown
rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "smart" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Gary is cold.[(triple1 OR ((triple4) -> rule3) OR ((triple4) -> rule4))] Gary is green.[(triple2)] Gary is nice.[(triple3)] Gary is white.[(triple4)] Harry is blue.[(triple5)] Harry is green.[(triple6)] Harry is white.[(triple7)] @1: Gary is quiet.[(((triple1) -> rule2) OR ((((triple4) -> rule3)) -> rule2) OR ((((triple4) -> rule4)) -> rule2))] Harry is cold.[(((triple7) -> rule3) OR ((triple7) -> rule4))] @2: Harry is quiet.[(((((triple7) -> rule3)) -> rule2) OR ((((triple7) -> rule4)) -> rule2))]
Gary is cold.
("Gary" "is" "cold" "+")
triple1
((triple4) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple4) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Gary is white.
("Gary" "is" "white" "+")
triple4
Harry is blue.
("Harry" "is" "blue" "+")
triple5
Harry is green.
("Harry" "is" "green" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((triple7) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple7) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple7) -> (rule4 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2