Anne is furry. Bob is smart. Charlie is white. Dave is furry. All green, smart things are red. If Anne is white and Anne is cold then Anne is furry. If something is cold and green then it is white. Round things are smart. If Anne is furry then Anne is white. Red, round things are cold. If something is white then it is round. All smart, round things are cold.
Anne is furry.
("Anne" "is" "furry" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is furry.
("Dave" "is" "furry" "+")
All green, smart things are red.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
If Anne is white and Anne is cold then Anne is furry.
((("Anne" "is" "white" "+") ("Anne" "is" "cold" "+")) -> ("Anne" "is" "furry" "+"))
If something is cold and green then it is white.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
Round things are smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
If Anne is furry then Anne is white.
((("Anne" "is" "furry" "+")) -> ("Anne" "is" "white" "+"))
Red, round things are cold.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If something is white then it is round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
All smart, round things are cold.
((("something" "is" "smart" "+") ("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
Charlie is white.
True
1
proof
[(triple3)]
("Charlie" "is" "white" "+")
triple3
Charlie is not white.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "white" "-")
triple3
Charlie is round.
True
2
proof
[(((triple3) -> rule7))]
("Charlie" "is" "round" "+")
((triple3) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple3) -> rule7))]
("Charlie" "is" "round" "-")
((triple3) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
True
3
proof
[(((((triple3) -> rule7)) -> rule4))]
("Charlie" "is" "smart" "+")
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is not smart.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule4))]
("Charlie" "is" "smart" "-")
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is cold.
True
6
proof
[(((((((triple3) -> rule7)) -> rule4) ((triple3) -> rule7)) -> rule8))]
("Charlie" "is" "cold" "+")
((((((triple3) -> (rule7 % int3))) -> (rule4 % int2)) ((triple3) -> (rule7 % int3))) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is not cold.
False
6
inv-proof
[(((((((triple3) -> rule7)) -> rule4) ((triple3) -> rule7)) -> rule8))]
("Charlie" "is" "cold" "-")
((((((triple3) -> (rule7 % int3))) -> (rule4 % int2)) ((triple3) -> (rule7 % int3))) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "white" "-")
Dave is white.
Unknown
rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "white" "+")
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "red" "-")
Dave is smart.
Unknown
rconc
[@3: Dave is smart.[CWA. Example of deepest failure = (rule4 <- rule7 <- rule3 <- FAIL)]]
("Dave" "is" "smart" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Anne is furry.[(triple1)] Bob is smart.[(triple2)] Charlie is white.[(triple3)] Dave is furry.[(triple4)] @1: Anne is white.[(((triple1) -> rule5))] Charlie is round.[(((triple3) -> rule7))] @2: Anne is round.[(((((triple1) -> rule5)) -> rule7))] Charlie is smart.[(((((triple3) -> rule7)) -> rule4))] @3: Anne is smart.[(((((((triple1) -> rule5)) -> rule7)) -> rule4))] Charlie is cold.[(((((((triple3) -> rule7)) -> rule4) ((triple3) -> rule7)) -> rule8))] @4: Anne is cold.[(((((((((triple1) -> rule5)) -> rule7)) -> rule4) ((((triple1) -> rule5)) -> rule7)) -> rule8))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple3) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
((((((triple3) -> (rule7 % int3))) -> (rule4 % int2)) ((triple3) -> (rule7 % int3))) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
((((((((triple1) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule4 % int2)) ((((triple1) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4