Anne is round. Bob is round. Charlie is red. Dave is red. Blue, red things are round. All red, furry things are round. All smart things are blue. If Dave is cold then Dave is round. If something is red then it is smart. If Charlie is nice then Charlie is cold.
Anne is round.
("Anne" "is" "round" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is red.
("Dave" "is" "red" "+")
Blue, red things are round.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
All red, furry things are round.
((("something" "is" "red" "+") ("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
All smart things are blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
If Dave is cold then Dave is round.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "round" "+"))
If something is red then it is smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
If Charlie is nice then Charlie is cold.
((("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "cold" "+"))
Anne is round.
True
1
proof
[(triple1)]
("Anne" "is" "round" "+")
triple1
Bob is not round.
False
1
inv-proof
[(triple2)]
("Bob" "is" "round" "-")
triple2
Dave is smart.
True
2
proof
[(((triple4) -> rule5))]
("Dave" "is" "smart" "+")
((triple4) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple4) -> rule5))]
("Dave" "is" "smart" "-")
((triple4) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Charlie is blue.
True
3
proof
[(((((triple3) -> rule5)) -> rule3))]
("Charlie" "is" "blue" "+")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Dave is not blue.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule3))]
("Dave" "is" "blue" "-")
((((triple4) -> (rule5 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Charlie is round.
True
5
proof
[(((((((triple3) -> rule5)) -> rule3) triple3) -> rule1))]
("Charlie" "is" "round" "+")
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2)) triple3) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Dave is not round.
False
5
inv-proof
[(((((((triple4) -> rule5)) -> rule3) triple4) -> rule1))]
("Dave" "is" "round" "-")
((((((triple4) -> (rule5 % int3))) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "smart" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "cold" "+")
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "smart" "-")
Bob is blue.
Unknown
rconc
[@2: Bob is blue.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Bob" "is" "blue" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Anne is round.[(triple1)] Bob is round.[(triple2)] Charlie is red.[(triple3)] Dave is red.[(triple4)] @1: Charlie is smart.[(((triple3) -> rule5))] Dave is smart.[(((triple4) -> rule5))] @2: Charlie is blue.[(((((triple3) -> rule5)) -> rule3))] Dave is blue.[(((((triple4) -> rule5)) -> rule3))] @3: Charlie is round.[(((((((triple3) -> rule5)) -> rule3) triple3) -> rule1))] Dave is round.[(((((((triple4) -> rule5)) -> rule3) triple4) -> rule1))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple3) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple4) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((((triple4) -> (rule5 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2)) triple3) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
((((((triple4) -> (rule5 % int3))) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3