Bob is kind. Erin is green. Gary is big. Harry is white. Big people are green. If Gary is green and Gary is not big then Gary is nice. If someone is big and not white then they are quiet. If someone is green and not white then they are quiet. If Gary is green then Gary is cold. If Harry is not white and Harry is not quiet then Harry is not cold. If someone is nice and not white then they are kind. All cold, green people are kind.
Bob is kind.
("Bob" "is" "kind" "+")
Erin is green.
("Erin" "is" "green" "+")
Gary is big.
("Gary" "is" "big" "+")
Harry is white.
("Harry" "is" "white" "+")
Big people are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If Gary is green and Gary is not big then Gary is nice.
((("Gary" "is" "green" "+") ("Gary" "is" "big" "~")) -> ("Gary" "is" "nice" "+"))
If someone is big and not white then they are quiet.
((("someone" "is" "big" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "quiet" "+"))
If someone is green and not white then they are quiet.
((("someone" "is" "green" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "quiet" "+"))
If Gary is green then Gary is cold.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "cold" "+"))
If Harry is not white and Harry is not quiet then Harry is not cold.
((("Harry" "is" "white" "~") ("Harry" "is" "quiet" "~")) -> ("Harry" "is" "cold" "-"))
If someone is nice and not white then they are kind.
((("someone" "is" "nice" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "kind" "+"))
All cold, green people are kind.
((("someone" "is" "cold" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
Bob is kind.
True
1
proof
[(triple1)]
("Bob" "is" "kind" "+")
triple1
Erin is not green.
False
1
inv-proof
[(triple2)]
("Erin" "is" "green" "-")
triple2
Gary is green.
True
2
proof
[(((triple3) -> rule1))]
("Gary" "is" "green" "+")
((triple3) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not green.
False
2
inv-proof
[(((triple3) -> rule1))]
("Gary" "is" "green" "-")
((triple3) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
True
3
proof
[(((((triple3) -> rule1)) -> rule5))]
("Gary" "is" "cold" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not cold.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule5))]
("Gary" "is" "cold" "-")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is kind.
True
6
proof
[(((((((triple3) -> rule1)) -> rule5) ((triple3) -> rule1)) -> rule8))]
("Gary" "is" "kind" "+")
((((((triple3) -> (rule1 % int3))) -> (rule5 % int2)) ((triple3) -> (rule1 % int3))) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is not kind.
False
6
inv-proof
[(((((((triple3) -> rule1)) -> rule5) ((triple3) -> rule1)) -> rule8))]
("Gary" "is" "kind" "-")
((((((triple3) -> (rule1 % int3))) -> (rule5 % int2)) ((triple3) -> (rule1 % int3))) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "green" "-")
Harry is quiet.
Unknown
rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "quiet" "+")
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "quiet" "-")
Harry is kind.
Unknown
rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "kind" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
@0: Bob is kind.[(triple1)] Erin is green.[(triple2)] Gary is big.[(triple3)] Harry is white.[(triple4)] @1: Gary is green.[(((triple3) -> rule1))] @2: Gary is cold.[(((((triple3) -> rule1)) -> rule5))] @3: Gary is kind.[(((((((triple3) -> rule1)) -> rule5) ((triple3) -> rule1)) -> rule8))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
Gary is big.
("Gary" "is" "big" "+")
triple3
Harry is white.
("Harry" "is" "white" "+")
triple4
Gary is green.
("Gary" "is" "green" "+")
((triple3) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((((((triple3) -> (rule1 % int3))) -> (rule5 % int2)) ((triple3) -> (rule1 % int3))) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3