Bob is cold. Dave is white. Erin is smart. Gary is furry. If something is rough then it is smart. Rough, green things are smart. All cold things are rough. If Bob is smart and Bob is rough then Bob is cold. Smart, cold things are round. If something is green then it is round. Rough, cold things are not white. White, green things are not cold.
Bob is cold.
("Bob" "is" "cold" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is furry.
("Gary" "is" "furry" "+")
If something is rough then it is smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
Rough, green things are smart.
((("something" "is" "rough" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
All cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If Bob is smart and Bob is rough then Bob is cold.
((("Bob" "is" "smart" "+") ("Bob" "is" "rough" "+")) -> ("Bob" "is" "cold" "+"))
Smart, cold things are round.
((("something" "is" "smart" "+") ("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If something is green then it is round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Rough, cold things are not white.
((("something" "is" "rough" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "-"))
White, green things are not cold.
((("something" "is" "white" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "-"))
Dave is white.
True
1
proof
[(triple2)]
("Dave" "is" "white" "+")
triple2
Dave is not white.
False
1
inv-proof
[(triple2)]
("Dave" "is" "white" "-")
triple2
Bob is rough.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "rough" "-")
((triple1) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not white.
True
4
proof
[(((((triple1) -> rule3) triple1) -> rule7))]
("Bob" "is" "white" "-")
((((triple1) -> (rule3 % int2)) triple1) -> (rule7 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is white.
False
4
inv-proof
[(((((triple1) -> rule3) triple1) -> rule7))]
("Bob" "is" "white" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule7 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is round.
True
5
proof
[(((((((triple1) -> rule3)) -> rule1) triple1) -> rule5))]
("Bob" "is" "round" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is not round.
False
5
inv-proof
[(((((((triple1) -> rule3)) -> rule1) triple1) -> rule5))]
("Bob" "is" "round" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is rough.
Unknown
rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "rough" "+")
Erin is not round.
Unknown
inv-rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "round" "-")
Gary is smart.
Unknown
rconc
[@2: Gary is smart.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Gary" "is" "smart" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Bob is cold.[(triple1)] Dave is white.[(triple2)] Erin is smart.[(triple3)] Gary is furry.[(triple4)] @1: Bob is rough.[(((triple1) -> rule3))] @2: Bob is not white.[(((((triple1) -> rule3) triple1) -> rule7))] Bob is smart.[(((((triple1) -> rule3)) -> rule1))] @3: Bob is round.[(((((((triple1) -> rule3)) -> rule1) triple1) -> rule5))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Gary is furry.
("Gary" "is" "furry" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not white.
("Bob" "is" "white" "-")
((((triple1) -> (rule3 % int2)) triple1) -> (rule7 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3