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