Bob is round. Charlie is blue. Dave is not kind. Erin is red. If someone is big and cold then they are not round. If someone is nice then they are round. Cold, blue people are round. All round people are not red. Kind people are nice. All blue people are nice. If Dave is not blue then Dave is kind. Cold people are not kind.
Bob is round.
("Bob" "is" "round" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Dave is not kind.
("Dave" "is" "kind" "-")
Erin is red.
("Erin" "is" "red" "+")
If someone is big and cold then they are not round.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "round" "-"))
If someone is nice then they are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
Cold, blue people are round.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
All round people are not red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "-"))
Kind people are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
All blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If Dave is not blue then Dave is kind.
((("Dave" "is" "blue" "~")) -> ("Dave" "is" "kind" "+"))
Cold people are not kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "-"))
Bob is round.
True
1
proof
[(triple1)]
("Bob" "is" "round" "+")
triple1
Dave is kind.
False
1
inv-proof
[(triple3)]
("Dave" "is" "kind" "+")
triple3
Charlie is nice.
True
2
proof
[(((triple2) -> rule6))]
("Charlie" "is" "nice" "+")
((triple2) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple2) -> rule6))]
("Charlie" "is" "nice" "-")
((triple2) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is round.
True
3
proof
[(((((triple2) -> rule6)) -> rule2))]
("Charlie" "is" "round" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not round.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule2))]
("Charlie" "is" "round" "-")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not red.
True
4
proof
[(((((((triple2) -> rule6)) -> rule2)) -> rule4))]
("Charlie" "is" "red" "-")
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is red.
False
4
inv-proof
[(((((((triple2) -> rule6)) -> rule2)) -> rule4))]
("Charlie" "is" "red" "+")
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "nice" "-")
Dave is nice.
Unknown
rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "nice" "+")
Erin is not nice.
Unknown
inv-rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "nice" "-")
Erin is round.
Unknown
rconc
[@2: Erin is round.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Erin" "is" "round" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Bob is round.[(triple1)] Charlie is blue.[(triple2)] Dave is not kind.[(triple3)] Erin is red.[(triple4)] @1: Bob is not red.[(((triple1) -> rule4))] Charlie is nice.[(((triple2) -> rule6))] @2: Charlie is round.[(((((triple2) -> rule6)) -> rule2))] @3: Charlie is not red.[(((((((triple2) -> rule6)) -> rule2)) -> rule4))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Dave is not kind.
("Dave" "is" "kind" "-")
triple3
Erin is red.
("Erin" "is" "red" "+")
triple4
Bob is not red.
("Bob" "is" "red" "-")
((triple1) -> (rule4 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple2) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not red.
("Charlie" "is" "red" "-")
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3