Bob is quiet. Bob is round. Dave is big. Dave is smart. Erin is green. Erin is smart. Fiona is cold. Round, smart things are quiet. If something is cold and round then it is green. If something is green then it is round.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Round, smart things are quiet.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If something is cold and round then it is green.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If something is green then it is round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Dave is big.
True
1
proof
[(triple3)]
("Dave" "is" "big" "+")
triple3
Bob is not quiet.
False
1
inv-proof
[(triple1)]
("Bob" "is" "quiet" "-")
triple1
Erin is round.
True
2
proof
[(((triple5) -> rule3))]
("Erin" "is" "round" "+")
((triple5) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not round.
False
2
inv-proof
[(((triple5) -> rule3))]
("Erin" "is" "round" "-")
((triple5) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
True
4
proof
[(((((triple5) -> rule3) triple6) -> rule1))]
("Erin" "is" "quiet" "+")
((((triple5) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not quiet.
False
4
inv-proof
[(((((triple5) -> rule3) triple6) -> rule1))]
("Erin" "is" "quiet" "-")
((((triple5) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Fiona is not green.
Unknown
inv-rconc
[@2: Fiona is green.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Fiona" "is" "green" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "green" "+")
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "green" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Bob is quiet.[(triple1)] Bob is round.[(triple2)] Dave is big.[(triple3)] Dave is smart.[(triple4)] Erin is green.[(triple5)] Erin is smart.[(triple6)] Fiona is cold.[(triple7)] @1: Erin is round.[(((triple5) -> rule3))] @2: Erin is quiet.[(((((triple5) -> rule3) triple6) -> rule1))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple4
Erin is green.
("Erin" "is" "green" "+")
triple5
Erin is smart.
("Erin" "is" "smart" "+")
triple6
Fiona is cold.
("Fiona" "is" "cold" "+")
triple7
Erin is round.
("Erin" "is" "round" "+")
((triple5) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple5) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2