Bob is red. Bob is round. Charlie is green. Charlie is white. Dave is blue. Dave is green. Fiona is kind. If something is green then it is nice. All nice things are round. All green things are round. Blue, green things are kind. Kind things are blue. If something is white then it is blue.
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
If something is green then it is nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
All nice things are round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
All green things are round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Blue, green things are kind.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
Kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If something is white then it is blue.
((("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
Dave is green.
True
1
proof
[(triple6)]
("Dave" "is" "green" "+")
triple6
Dave is not blue.
False
1
inv-proof
[(triple5)]
("Dave" "is" "blue" "-")
triple5
Bob is not blue.
Unknown
inv-rconc
[@2: Bob is blue.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Bob" "is" "blue" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Bob is red.[(triple1)] Bob is round.[(triple2)] Charlie is green.[(triple3)] Charlie is white.[(triple4)] Dave is blue.[(triple5)] Dave is green.[(triple6)] Fiona is kind.[(triple7)] @1: Charlie is blue.[(((triple4) -> rule6))] Charlie is nice.[(((triple3) -> rule1))] Charlie is round.[(((triple3) -> rule3) OR ((((triple3) -> rule1)) -> rule2))] Dave is kind.[(((triple5 triple6) -> rule4))] Dave is nice.[(((triple6) -> rule1))] Dave is round.[(((triple6) -> rule3) OR ((((triple6) -> rule1)) -> rule2))] Fiona is blue.[(((triple7) -> rule5))] @2: Charlie is kind.[(((((triple4) -> rule6) triple3) -> rule4))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Dave is blue.
("Dave" "is" "blue" "+")
triple5
Dave is green.
("Dave" "is" "green" "+")
triple6
Fiona is kind.
("Fiona" "is" "kind" "+")
triple7
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple4) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple3) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((triple5 triple6) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple6) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple6) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple7) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple4) -> (rule6 % int2)) triple3) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2