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