Bob is white. Charlie is nice. Dave is smart. White people are round. If Dave is cold then Dave is white. If Charlie is green and Charlie is white then Charlie is smart. All round people are nice. If Dave is round and Dave is nice then Dave is smart. All nice people are green. Nice people are smart. All round people are white.
Bob is white.
("Bob" "is" "white" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is smart.
("Dave" "is" "smart" "+")
White people are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
If Dave is cold then Dave is white.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "white" "+"))
If Charlie is green and Charlie is white then Charlie is smart.
((("Charlie" "is" "green" "+") ("Charlie" "is" "white" "+")) -> ("Charlie" "is" "smart" "+"))
All round people are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
If Dave is round and Dave is nice then Dave is smart.
((("Dave" "is" "round" "+") ("Dave" "is" "nice" "+")) -> ("Dave" "is" "smart" "+"))
All nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
Nice people are smart.
((("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
All round people are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
Bob is white.
True
1
proof
[(triple1)]
("Bob" "is" "white" "+")
triple1
Charlie is not nice.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "nice" "-")
triple2
Bob is round.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "round" "+")
((triple1) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple2) -> rule6))]
("Charlie" "is" "green" "-")
((triple2) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Bob is nice.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("Bob" "is" "nice" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is not nice.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule4))]
("Bob" "is" "nice" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
True
4
proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule6))]
("Bob" "is" "green" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is not smart.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule7))]
("Bob" "is" "smart" "-")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Dave is not nice.
Unknown
inv-rconc
[@3: Dave is nice.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule2 <- FAIL)]]
("Dave" "is" "nice" "-")
Dave is green.
Unknown
rconc
[@4: Dave is green.[CWA. Example of deepest failure = (rule6 <- rule4 <- rule1 <- rule2 <- FAIL)]]
("Dave" "is" "green" "+")
Dave is not white.
Unknown
inv-rconc
[@3: Dave is white.[CWA. Example of deepest failure = (rule8 <- rule1 <- rule2 <- FAIL)]]
("Dave" "is" "white" "-")
Charlie is round.
Unknown
rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("Charlie" "is" "round" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Bob is white.[(triple1)] Charlie is nice.[(triple2)] Dave is smart.[(triple3)] @1: Bob is round.[(((triple1) -> rule1))] Charlie is green.[(((triple2) -> rule6))] Charlie is smart.[(((triple2) -> rule7))] @2: Bob is nice.[(((((triple1) -> rule1)) -> rule4))] @3: Bob is green.[(((((((triple1) -> rule1)) -> rule4)) -> rule6))] Bob is smart.[(((((((triple1) -> rule1)) -> rule4)) -> rule7))]
Bob is white.
("Bob" "is" "white" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple2) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2) -> (rule7 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3