Bob is green. Bob is kind. Charlie is green. Charlie is smart. Dave is kind. Dave is round. Fiona is round. All white, smart things are rough. All rough, green things are round. If Dave is white and Dave is rough then Dave is furry. Green, kind things are white. Kind things are smart. All white, rough things are smart.
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
Fiona is round.
("Fiona" "is" "round" "+")
All white, smart things are rough.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
All rough, green things are round.
((("something" "is" "rough" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If Dave is white and Dave is rough then Dave is furry.
((("Dave" "is" "white" "+") ("Dave" "is" "rough" "+")) -> ("Dave" "is" "furry" "+"))
Green, kind things are white.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Kind things are smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
All white, rough things are smart.
((("something" "is" "white" "+") ("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
Dave is round.
True
1
proof
[(triple6)]
("Dave" "is" "round" "+")
triple6
Charlie is not green.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "green" "-")
triple3
Dave is smart.
True
2
proof
[(((triple5) -> rule5))]
("Dave" "is" "smart" "+")
((triple5) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Bob is not smart.
False
2
inv-proof
[(((triple2) -> rule5))]
("Bob" "is" "smart" "-")
((triple2) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is rough.
True
6
proof
[(((((triple1 triple2) -> rule4) ((triple2) -> rule5)) -> rule1))]
("Bob" "is" "rough" "+")
((((triple1 triple2) -> (rule4 % int3)) ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not rough.
False
6
inv-proof
[(((((triple1 triple2) -> rule4) ((triple2) -> rule5)) -> rule1))]
("Bob" "is" "rough" "-")
((((triple1 triple2) -> (rule4 % int3)) ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is round.
True
8
proof
[(((((((triple1 triple2) -> rule4) ((triple2) -> rule5)) -> rule1) triple1) -> rule2))]
("Bob" "is" "round" "+")
((((((triple1 triple2) -> (rule4 % int4)) ((triple2) -> (rule5 % int3))) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is not round.
False
8
inv-proof
[(((((((triple1 triple2) -> rule4) ((triple2) -> rule5)) -> rule1) triple1) -> rule2))]
("Bob" "is" "round" "-")
((((((triple1 triple2) -> (rule4 % int4)) ((triple2) -> (rule5 % int3))) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Dave is not rough.
Unknown
inv-rconc
[@2: Dave is rough.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Dave" "is" "rough" "-")
Dave is white.
Unknown
rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "white" "+")
Fiona is not smart.
Unknown
inv-rconc
[@2: Fiona is smart.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is rough.
Unknown
rconc
[@2: Fiona is rough.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Fiona" "is" "rough" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Bob is green.[(triple1)] Bob is kind.[(triple2)] Charlie is green.[(triple3)] Charlie is smart.[(triple4)] Dave is kind.[(triple5)] Dave is round.[(triple6)] Fiona is round.[(triple7)] @1: Bob is smart.[(((triple2) -> rule5))] Bob is white.[(((triple1 triple2) -> rule4))] Dave is smart.[(((triple5) -> rule5))] @2: Bob is rough.[(((((triple1 triple2) -> rule4) ((triple2) -> rule5)) -> rule1))] @3: Bob is round.[(((((((triple1 triple2) -> rule4) ((triple2) -> rule5)) -> rule1) triple1) -> rule2))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
Fiona is round.
("Fiona" "is" "round" "+")
triple7
Bob is smart.
("Bob" "is" "smart" "+")
((triple2) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple1 triple2) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple5) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((((triple1 triple2) -> (rule4 % int3)) ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
((((((triple1 triple2) -> (rule4 % int4)) ((triple2) -> (rule5 % int3))) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4