Bob is not blue. Bob is kind. Bob is round. Bob is smart. Bob is white. Dave is red. Dave is smart. Gary is round. Gary is not white. Harry is white. If something is white then it is red. All blue things are not red. All smart things are red. Blue things are smart. If something is cold and not kind then it is smart. Red things are smart. If Gary is kind then Gary is red. All red things are white.
Bob is not blue.
("Bob" "is" "blue" "-")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is not white.
("Gary" "is" "white" "-")
Harry is white.
("Harry" "is" "white" "+")
If something is white then it is red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
All blue things are not red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "-"))
All smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
If something is cold and not kind then it is smart.
((("something" "is" "cold" "+") ("something" "is" "kind" "~")) -> ("something" "is" "smart" "+"))
Red things are smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
If Gary is kind then Gary is red.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "red" "+"))
All red things are white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
Bob is kind.
True
1
proof
[(triple2)]
("Bob" "is" "kind" "+")
triple2
Dave is not red.
False
1
inv-proof
[(triple6 OR ((triple7) -> rule3))]
("Dave" "is" "red" "-")
triple6
((triple7) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
True
2
proof
[(((triple6) -> rule8) OR ((((triple7) -> rule3)) -> rule8))]
("Dave" "is" "white" "+")
((triple6) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not white.
False
2
inv-proof
[(((triple6) -> rule8) OR ((((triple7) -> rule3)) -> rule8))]
("Dave" "is" "white" "-")
((triple6) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Gary is not red.
Unknown
inv-rconc
[@3: Gary is red.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule1 <- FAIL)]]
("Gary" "is" "red" "-")
Gary is smart.
Unknown
rconc
[@3: Gary is smart.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule4 <- FAIL)]]
("Gary" "is" "smart" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Bob is kind.[(triple2)] Bob is not blue.[(triple1)] Bob is round.[(triple3)] Bob is smart.[(triple4 OR ((((triple5) -> rule1)) -> rule6))] Bob is white.[(triple5 OR ((((triple4) -> rule3)) -> rule8))] Dave is red.[(triple6 OR ((triple7) -> rule3))] Dave is smart.[(triple7 OR ((triple6) -> rule6))] Gary is not white.[(triple9)] Gary is round.[(triple8)] Harry is white.[(triple10)] @1: Bob is red.[(((triple4) -> rule3) OR ((triple5) -> rule1))] Dave is white.[(((triple6) -> rule8) OR ((((triple7) -> rule3)) -> rule8))] Harry is red.[(((triple10) -> rule1))] @2: Harry is smart.[(((((triple10) -> rule1)) -> rule6))]
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is not blue.
("Bob" "is" "blue" "-")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
((((triple5) -> (rule1 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
triple5
((((triple4) -> (rule3 % int2))) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple6
((triple7) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple7
((triple6) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Gary is not white.
("Gary" "is" "white" "-")
triple9
Gary is round.
("Gary" "is" "round" "+")
triple8
Harry is white.
("Harry" "is" "white" "+")
triple10
Bob is red.
("Bob" "is" "red" "+")
((triple4) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple5) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple6) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((triple10) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((((triple10) -> (rule1 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2