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