Anne is quiet. Bob is smart. Gary is rough. Harry is not rough. If Bob is quiet and Bob is blue then Bob is kind. Smart things are quiet. If something is blue then it is kind. If something is cold and not rough then it is not kind. Smart, blue things are not cold. All rough things are cold. Cold things are smart. If something is smart and not cold then it is not nice.
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
If Bob is quiet and Bob is blue then Bob is kind.
((("Bob" "is" "quiet" "+") ("Bob" "is" "blue" "+")) -> ("Bob" "is" "kind" "+"))
Smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If something is blue then it is kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If something is cold and not rough then it is not kind.
((("something" "is" "cold" "+") ("something" "is" "rough" "~")) -> ("something" "is" "kind" "-"))
Smart, blue things are not cold.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "-"))
All rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
Cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If something is smart and not cold then it is not nice.
((("something" "is" "smart" "+") ("something" "is" "cold" "~")) -> ("something" "is" "nice" "-"))
Gary is rough.
True
1
proof
[(triple3)]
("Gary" "is" "rough" "+")
triple3
Harry is rough.
False
1
inv-proof
[(triple4)]
("Harry" "is" "rough" "+")
triple4
Gary is cold.
True
2
proof
[(((triple3) -> rule6))]
("Gary" "is" "cold" "+")
((triple3) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not cold.
False
2
inv-proof
[(((triple3) -> rule6))]
("Gary" "is" "cold" "-")
((triple3) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
True
3
proof
[(((((triple3) -> rule6)) -> rule7))]
("Gary" "is" "smart" "+")
((((triple3) -> (rule6 % int2))) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not smart.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule7))]
("Gary" "is" "smart" "-")
((((triple3) -> (rule6 % int2))) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is quiet.
True
4
proof
[(((((((triple3) -> rule6)) -> rule7)) -> rule2))]
("Gary" "is" "quiet" "+")
((((((triple3) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is not quiet.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule7)) -> rule2))]
("Gary" "is" "quiet" "-")
((((((triple3) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "cold" "-")
Anne is cold.
Unknown
rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "cold" "+")
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "kind" "-")
Gary is kind.
Unknown
rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "kind" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Anne is quiet.[(triple1)] Bob is smart.[(triple2)] Gary is rough.[(triple3)] Harry is not rough.[(triple4)] @1: Bob is quiet.[(((triple2) -> rule2))] Gary is cold.[(((triple3) -> rule6))] @2: Gary is smart.[(((((triple3) -> rule6)) -> rule7))] @3: Gary is quiet.[(((((((triple3) -> rule6)) -> rule7)) -> rule2))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Gary is rough.
("Gary" "is" "rough" "+")
triple3
Harry is not rough.
("Harry" "is" "rough" "-")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple3) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((((triple3) -> (rule6 % int2))) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((((triple3) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3