Bob is green. Bob is kind. Bob is red. Bob is round. Charlie is cold. Charlie is green. Charlie is kind. Charlie is not nice. Charlie is round. Erin is not cold. Erin is not kind. Erin is nice. If someone is red and green then they are cold. Red people are white. If someone is green then they are red.
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is not nice.
("Charlie" "is" "nice" "-")
Charlie is round.
("Charlie" "is" "round" "+")
Erin is not cold.
("Erin" "is" "cold" "-")
Erin is not kind.
("Erin" "is" "kind" "-")
Erin is nice.
("Erin" "is" "nice" "+")
If someone is red and green then they are cold.
((("someone" "is" "red" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
Red people are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
If someone is green then they are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
Charlie is not nice.
True
1
proof
[(triple8)]
("Charlie" "is" "nice" "-")
triple8
Charlie is nice.
False
1
inv-proof
[(triple8)]
("Charlie" "is" "nice" "+")
triple8
Bob is cold.
True
3
proof
[(((triple3 triple1) -> rule1) OR ((((triple1) -> rule3) triple1) -> rule1))]
("Bob" "is" "cold" "+")
((triple3 triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not white.
False
2
inv-proof
[(((triple3) -> rule2) OR ((((triple1) -> rule3)) -> rule2))]
("Bob" "is" "white" "-")
((triple3) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "red" "-")
Erin is white.
Unknown
rconc
[@2: Erin is white.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Erin" "is" "white" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Bob is green.[(triple1)] Bob is kind.[(triple2)] Bob is red.[(triple3 OR ((triple1) -> rule3))] Bob is round.[(triple4)] Charlie is cold.[(triple5 OR ((((triple6) -> rule3) triple6) -> rule1))] Charlie is green.[(triple6)] Charlie is kind.[(triple7)] Charlie is not nice.[(triple8)] Charlie is round.[(triple9)] Erin is nice.[(triple12)] Erin is not cold.[(triple10)] Erin is not kind.[(triple11)] @1: Bob is cold.[(((triple3 triple1) -> rule1) OR ((((triple1) -> rule3) triple1) -> rule1))] Bob is white.[(((triple3) -> rule2) OR ((((triple1) -> rule3)) -> rule2))] Charlie is red.[(((triple6) -> rule3))] @2: Charlie is white.[(((((triple6) -> rule3)) -> rule2))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
((triple1) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple4
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
((((triple6) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
triple6
Charlie is kind.
("Charlie" "is" "kind" "+")
triple7
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple8
Charlie is round.
("Charlie" "is" "round" "+")
triple9
Erin is nice.
("Erin" "is" "nice" "+")
triple12
Erin is not cold.
("Erin" "is" "cold" "-")
triple10
Erin is not kind.
("Erin" "is" "kind" "-")
triple11
Bob is cold.
("Bob" "is" "cold" "+")
((triple3 triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((triple3) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((triple6) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2