Bob is round. Charlie is round. Dave is smart. Fiona is white. If someone is round then they are white. All kind people are blue. If Charlie is cold and Charlie is smart then Charlie is kind. If someone is white and round then they are kind. If Charlie is quiet then Charlie is smart. All white, blue people are round. If Dave is white and Dave is blue then Dave is round. If Charlie is smart and Charlie is round then Charlie is kind.
Bob is round.
("Bob" "is" "round" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If someone is round then they are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
All kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If Charlie is cold and Charlie is smart then Charlie is kind.
((("Charlie" "is" "cold" "+") ("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "kind" "+"))
If someone is white and round then they are kind.
((("someone" "is" "white" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
If Charlie is quiet then Charlie is smart.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "smart" "+"))
All white, blue people are round.
((("someone" "is" "white" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If Dave is white and Dave is blue then Dave is round.
((("Dave" "is" "white" "+") ("Dave" "is" "blue" "+")) -> ("Dave" "is" "round" "+"))
If Charlie is smart and Charlie is round then Charlie is kind.
((("Charlie" "is" "smart" "+") ("Charlie" "is" "round" "+")) -> ("Charlie" "is" "kind" "+"))
Charlie is round.
True
1
proof
[(triple2)]
("Charlie" "is" "round" "+")
triple2
Fiona is not white.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "white" "-")
triple4
Charlie is white.
True
2
proof
[(((triple2) -> rule1))]
("Charlie" "is" "white" "+")
((triple2) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Bob is not white.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "white" "-")
((triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is kind.
True
4
proof
[(((((triple2) -> rule1) triple2) -> rule4))]
("Charlie" "is" "kind" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Bob is not kind.
False
4
inv-proof
[(((((triple1) -> rule1) triple1) -> rule4))]
("Bob" "is" "kind" "-")
((((triple1) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Charlie is blue.
True
5
proof
[(((((((triple2) -> rule1) triple2) -> rule4)) -> rule2))]
("Charlie" "is" "blue" "+")
((((((triple2) -> (rule1 % int3)) triple2) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is not blue.
False
5
inv-proof
[(((((((triple2) -> rule1) triple2) -> rule4)) -> rule2))]
("Charlie" "is" "blue" "-")
((((((triple2) -> (rule1 % int3)) triple2) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "smart" "-")
Fiona is round.
Unknown
rconc
[@3: Fiona is round.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule4 <- FAIL)]]
("Fiona" "is" "round" "+")
Fiona is not kind.
Unknown
inv-rconc
[@3: Fiona is kind.[CWA. Example of deepest failure = (rule4 <- rule6 <- rule2 <- FAIL)]]
("Fiona" "is" "kind" "-")
Dave is round.
Unknown
rconc
[@3: Dave is round.[CWA. Example of deepest failure = (rule6 <- rule1 <- rule7 <- FAIL)]]
("Dave" "is" "round" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Bob is round.[(triple1)] Charlie is round.[(triple2)] Dave is smart.[(triple3)] Fiona is white.[(triple4)] @1: Bob is white.[(((triple1) -> rule1))] Charlie is white.[(((triple2) -> rule1))] @2: Bob is kind.[(((((triple1) -> rule1) triple1) -> rule4))] Charlie is kind.[(((((triple2) -> rule1) triple2) -> rule4))] @3: Bob is blue.[(((((((triple1) -> rule1) triple1) -> rule4)) -> rule2))] Charlie is blue.[(((((((triple2) -> rule1) triple2) -> rule4)) -> rule2))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Fiona is white.
("Fiona" "is" "white" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple2) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((((((triple1) -> (rule1 % int3)) triple1) -> (rule4 % int2))) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
((((((triple2) -> (rule1 % int3)) triple2) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3