Bob is green. Bob is rough. Bob is not smart. Bob is white. Dave is not green. Dave is not quiet. Dave is round. Dave is white. Erin is cold. Erin is quiet. Erin is rough. Erin is not round. Gary is quiet. Gary is not round. Gary is white. All white, cold people are green. If someone is white and not rough then they are not green. All smart people are green. If Erin is not quiet then Erin is cold. White, green people are cold. Quiet, white people are smart.
Bob is green.
("Bob" "is" "green" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Bob is white.
("Bob" "is" "white" "+")
Dave is not green.
("Dave" "is" "green" "-")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is not round.
("Erin" "is" "round" "-")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is not round.
("Gary" "is" "round" "-")
Gary is white.
("Gary" "is" "white" "+")
All white, cold people are green.
((("someone" "is" "white" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If someone is white and not rough then they are not green.
((("someone" "is" "white" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "green" "-"))
All smart people are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If Erin is not quiet then Erin is cold.
((("Erin" "is" "quiet" "~")) -> ("Erin" "is" "cold" "+"))
White, green people are cold.
((("someone" "is" "white" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
Quiet, white people are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
Dave is round.
True
1
proof
[(triple7)]
("Dave" "is" "round" "+")
triple7
Erin is round.
False
1
inv-proof
[(triple12)]
("Erin" "is" "round" "+")
triple12
Bob is cold.
True
3
proof
[(((triple4 triple1) -> rule5))]
("Bob" "is" "cold" "+")
((triple4 triple1) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Gary is not smart.
False
3
inv-proof
[(((triple13 triple15) -> rule6))]
("Gary" "is" "smart" "-")
((triple13 triple15) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is green.
True
4
proof
[(((((triple13 triple15) -> rule6)) -> rule3))]
("Gary" "is" "green" "+")
((((triple13 triple15) -> (rule6 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not green.
False
4
inv-proof
[(((((triple13 triple15) -> rule6)) -> rule3))]
("Gary" "is" "green" "-")
((((triple13 triple15) -> (rule6 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is cold.
True
6
proof
[(((triple15 ((((triple13 triple15) -> rule6)) -> rule3)) -> rule5))]
("Gary" "is" "cold" "+")
((triple15 ((((triple13 triple15) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not cold.
False
6
inv-proof
[(((triple15 ((((triple13 triple15) -> rule6)) -> rule3)) -> rule5))]
("Gary" "is" "cold" "-")
((triple15 ((((triple13 triple15) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Erin is not green.
Unknown
inv-rconc
[@2: Erin is green.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Erin" "is" "green" "-")
Erin is smart.
Unknown
rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "smart" "+")
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "cold" "-")
Dave is smart.
Unknown
rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "smart" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Bob is green.[(triple1)] Bob is not smart.[(triple3)] Bob is rough.[(triple2)] Bob is white.[(triple4)] Dave is not green.[(triple5)] Dave is not quiet.[(triple6)] Dave is round.[(triple7)] Dave is white.[(triple8)] Erin is cold.[(triple9)] Erin is not round.[(triple12)] Erin is quiet.[(triple10)] Erin is rough.[(triple11)] Gary is not round.[(triple14)] Gary is quiet.[(triple13)] Gary is white.[(triple15)] @1: Bob is cold.[(((triple4 triple1) -> rule5))] Gary is smart.[(((triple13 triple15) -> rule6))] @2: Gary is green.[(((((triple13 triple15) -> rule6)) -> rule3))] @3: Gary is cold.[(((triple15 ((((triple13 triple15) -> rule6)) -> rule3)) -> rule5))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is not smart.
("Bob" "is" "smart" "-")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple4
Dave is not green.
("Dave" "is" "green" "-")
triple5
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple6
Dave is round.
("Dave" "is" "round" "+")
triple7
Dave is white.
("Dave" "is" "white" "+")
triple8
Erin is cold.
("Erin" "is" "cold" "+")
triple9
Erin is not round.
("Erin" "is" "round" "-")
triple12
Erin is quiet.
("Erin" "is" "quiet" "+")
triple10
Erin is rough.
("Erin" "is" "rough" "+")
triple11
Gary is not round.
("Gary" "is" "round" "-")
triple14
Gary is quiet.
("Gary" "is" "quiet" "+")
triple13
Gary is white.
("Gary" "is" "white" "+")
triple15
Bob is cold.
("Bob" "is" "cold" "+")
((triple4 triple1) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple13 triple15) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((((triple13 triple15) -> (rule6 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((triple15 ((((triple13 triple15) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3