Anne is nice. Anne is round. Anne is smart. Anne is white. Charlie is blue. Charlie is nice. Charlie is quiet. Charlie is smart. Erin is nice. Erin is smart. Erin is white. Harry is nice. Harry is quiet. Harry is round. Harry is smart. Harry is white. Smart people are white. All smart people are nice. All blue people are nice. White, smart people are quiet. If Anne is blue and Anne is nice then Anne is round. Round, blue people are quiet. All white people are quiet. All quiet people are white.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Smart people are white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
All smart people are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
All blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
White, smart people are quiet.
((("someone" "is" "white" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
If Anne is blue and Anne is nice then Anne is round.
((("Anne" "is" "blue" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "round" "+"))
Round, blue people are quiet.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
All white people are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
All quiet people are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
Harry is nice.
True
1
proof
[(triple12 OR ((triple15) -> rule2))]
("Harry" "is" "nice" "+")
triple12
((triple15) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Anne is not nice.
False
1
inv-proof
[(triple1 OR ((triple3) -> rule2))]
("Anne" "is" "nice" "-")
triple1
((triple3) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Anne is nice.[(triple1 OR ((triple3) -> rule2))] Anne is round.[(triple2)] Anne is smart.[(triple3)] Anne is white.[(triple4 OR ((triple3) -> rule1))] Charlie is blue.[(triple5)] Charlie is nice.[(triple6 OR ((triple5) -> rule3) OR ((triple8) -> rule2))] Charlie is quiet.[(triple7 OR ((((triple8) -> rule1)) -> rule7) OR ((((triple8) -> rule1) triple8) -> rule4))] Charlie is smart.[(triple8)] Erin is nice.[(triple9 OR ((triple10) -> rule2))] Erin is smart.[(triple10)] Erin is white.[(triple11 OR ((triple10) -> rule1))] Harry is nice.[(triple12 OR ((triple15) -> rule2))] Harry is quiet.[(triple13 OR ((triple16) -> rule7) OR ((triple16 triple15) -> rule4) OR ((((triple15) -> rule1)) -> rule7) OR ((((triple15) -> rule1) triple15) -> rule4))] Harry is round.[(triple14)] Harry is smart.[(triple15)] Harry is white.[(triple16 OR ((triple13) -> rule8) OR ((triple15) -> rule1))] @1: Anne is quiet.[(((triple4) -> rule7) OR ((triple4 triple3) -> rule4) OR ((((triple3) -> rule1)) -> rule7) OR ((((triple3) -> rule1) triple3) -> rule4))] Charlie is white.[(((triple7) -> rule8) OR ((triple8) -> rule1))] Erin is quiet.[(((triple11) -> rule7) OR ((triple11 triple10) -> rule4) OR ((((triple10) -> rule1)) -> rule7) OR ((((triple10) -> rule1) triple10) -> rule4))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
((triple3) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
((triple3) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
((triple5) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((triple8) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple7
((((triple8) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((triple8) -> (rule1 % int2)) triple8) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple8
Erin is nice.
("Erin" "is" "nice" "+")
triple9
((triple10) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple10
Erin is white.
("Erin" "is" "white" "+")
triple11
((triple10) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple12
((triple15) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
((triple16) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple16 triple15) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple15) -> (rule1 % int2))) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple15) -> (rule1 % int2)) triple15) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Harry is white.
("Harry" "is" "white" "+")
triple16
((triple13) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple15) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple4) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((triple4 triple3) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((triple3) -> (rule1 % int2)) triple3) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((triple7) -> (rule8 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple8) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple11) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple11 triple10) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple10) -> (rule1 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple10) -> (rule1 % int2)) triple10) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2