Bob is blue. Bob is nice. Bob is quiet. Bob is red. Bob is round. Bob is white. Bob is young. Charlie is blue. Charlie is nice. Charlie is white. Harry is red. Harry is round. Red, nice people are round. Blue, nice people are red. If someone is nice then they are red. Red people are white. If Charlie is red then Charlie is blue. If Harry is young and Harry is quiet then Harry is nice.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Red, nice people are round.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
Blue, nice people are red.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If someone is nice then they are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
Red people are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
If Charlie is red then Charlie is blue.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "blue" "+"))
If Harry is young and Harry is quiet then Harry is nice.
((("Harry" "is" "young" "+") ("Harry" "is" "quiet" "+")) -> ("Harry" "is" "nice" "+"))
Bob is white.
True
1
proof
[(triple6 OR ((triple4) -> rule4) OR ((((triple2) -> rule3)) -> rule4) OR ((((triple1 triple2) -> rule2)) -> rule4))]
("Bob" "is" "white" "+")
triple6
((triple4) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple1 triple2) -> (rule2 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not red.
False
1
inv-proof
[(triple4 OR ((triple2) -> rule3) OR ((triple1 triple2) -> rule2))]
("Bob" "is" "red" "-")
triple4
((triple2) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple1 triple2) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "nice" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Bob is blue.[(triple1)] Bob is nice.[(triple2)] Bob is quiet.[(triple3)] Bob is red.[(triple4 OR ((triple2) -> rule3) OR ((triple1 triple2) -> rule2))] Bob is round.[(triple5 OR ((triple4 triple2) -> rule1) OR ((((triple2) -> rule3) triple2) -> rule1) OR ((((triple1 triple2) -> rule2) triple2) -> rule1))] Bob is white.[(triple6 OR ((triple4) -> rule4) OR ((((triple2) -> rule3)) -> rule4) OR ((((triple1 triple2) -> rule2)) -> rule4))] Bob is young.[(triple7)] Charlie is blue.[(triple8 OR ((((triple9) -> rule3)) -> rule5))] Charlie is nice.[(triple9)] Charlie is white.[(triple10 OR ((((triple9) -> rule3)) -> rule4) OR ((((triple8 triple9) -> rule2)) -> rule4))] Harry is red.[(triple11)] Harry is round.[(triple12)] @1: Charlie is red.[(((triple9) -> rule3) OR ((triple8 triple9) -> rule2))] Harry is white.[(((triple11) -> rule4))] @2: Charlie is round.[(((((triple9) -> rule3) triple9) -> rule1) OR ((((triple8 triple9) -> rule2) triple9) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
((triple2) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple1 triple2) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple5
((triple4 triple2) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((((triple2) -> (rule3 % int2)) triple2) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple1 triple2) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
triple6
((triple4) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple1 triple2) -> (rule2 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
triple7
Charlie is blue.
("Charlie" "is" "blue" "+")
triple8
((((triple9) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple9
Charlie is white.
("Charlie" "is" "white" "+")
triple10
((((triple9) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((triple8 triple9) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
Charlie is red.
("Charlie" "is" "red" "+")
((triple9) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple8 triple9) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple11) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((((triple9) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((triple8 triple9) -> (rule2 % int2)) triple9) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2