Bob is blue. Erin is round. Gary is kind. If something is nice then it is kind. If Bob is kind and Bob is green then Bob is quiet. Round things are nice. All blue things are round. Blue things are nice. All cold things are green.
Bob is blue.
("Bob" "is" "blue" "+")
Erin is round.
("Erin" "is" "round" "+")
Gary is kind.
("Gary" "is" "kind" "+")
If something is nice then it is kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If Bob is kind and Bob is green then Bob is quiet.
((("Bob" "is" "kind" "+") ("Bob" "is" "green" "+")) -> ("Bob" "is" "quiet" "+"))
Round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
All blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
Blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
All cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
Gary is kind.
True
1
proof
[(triple3)]
("Gary" "is" "kind" "+")
triple3
Bob is not blue.
False
1
inv-proof
[(triple1)]
("Bob" "is" "blue" "-")
triple1
Bob is nice.
True
2
proof
[(((triple1) -> rule5) OR ((((triple1) -> rule4)) -> rule3))]
("Bob" "is" "nice" "+")
((triple1) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Erin is not nice.
False
2
inv-proof
[(((triple2) -> rule3))]
("Erin" "is" "nice" "-")
((triple2) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is kind.
True
3
proof
[(((((triple2) -> rule3)) -> rule1))]
("Erin" "is" "kind" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Bob is not kind.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule1) OR ((((((triple1) -> rule4)) -> rule3)) -> rule1))]
("Bob" "is" "kind" "-")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "green" "-")
Gary is round.
Unknown
rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "round" "+")
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "green" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Bob is blue.[(triple1)] Erin is round.[(triple2)] Gary is kind.[(triple3)] @1: Bob is nice.[(((triple1) -> rule5) OR ((((triple1) -> rule4)) -> rule3))] Bob is round.[(((triple1) -> rule4))] Erin is nice.[(((triple2) -> rule3))] @2: Bob is kind.[(((((triple1) -> rule5)) -> rule1) OR ((((((triple1) -> rule4)) -> rule3)) -> rule1))] Erin is kind.[(((((triple2) -> rule3)) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Erin is round.
("Erin" "is" "round" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
((triple1) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2