Anne is blue. Anne is green. Anne is nice. Anne is red. Anne is round. Anne is smart. Anne is young. Charlie is blue. Charlie is green. Charlie is nice. Charlie is red. Charlie is smart. Charlie is young. Harry is blue. Harry is round. Harry is young. If Harry is young then Harry is blue. All green, young people are smart. Blue people are green.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is young then Harry is blue.
((("Harry" "is" "young" "+")) -> ("Harry" "is" "blue" "+"))
All green, young people are smart.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
Blue people are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Charlie is not blue.
False
1
inv-proof
[(triple8)]
("Charlie" "is" "blue" "-")
triple8
Harry is green.
True
2
proof
[(((triple14) -> rule3) OR ((((triple16) -> rule1)) -> rule3))]
("Harry" "is" "green" "+")
((triple14) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple16) -> (rule1 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not green.
False
2
inv-proof
[(((triple14) -> rule3) OR ((((triple16) -> rule1)) -> rule3))]
("Harry" "is" "green" "-")
((triple14) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple16) -> (rule1 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
True
4
proof
[(((((triple14) -> rule3) triple16) -> rule2) OR ((((((triple16) -> rule1)) -> rule3) triple16) -> rule2))]
("Harry" "is" "smart" "+")
((((triple14) -> (rule3 % int2)) triple16) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((((triple16) -> (rule1 % int3))) -> (rule3 % int2)) triple16) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is not smart.
False
4
inv-proof
[(((((triple14) -> rule3) triple16) -> rule2) OR ((((((triple16) -> rule1)) -> rule3) triple16) -> rule2))]
("Harry" "is" "smart" "-")
((((triple14) -> (rule3 % int2)) triple16) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((((triple16) -> (rule1 % int3))) -> (rule3 % int2)) triple16) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Anne is blue.[(triple1)] Anne is green.[(triple2 OR ((triple1) -> rule3))] Anne is nice.[(triple3)] Anne is red.[(triple4)] Anne is round.[(triple5)] Anne is smart.[(triple6 OR ((triple2 triple7) -> rule2) OR ((((triple1) -> rule3) triple7) -> rule2))] Anne is young.[(triple7)] Charlie is blue.[(triple8)] Charlie is green.[(triple9 OR ((triple8) -> rule3))] Charlie is nice.[(triple10)] Charlie is red.[(triple11)] Charlie is smart.[(triple12 OR ((triple9 triple13) -> rule2) OR ((((triple8) -> rule3) triple13) -> rule2))] Charlie is young.[(triple13)] Harry is blue.[(triple14 OR ((triple16) -> rule1))] Harry is round.[(triple15)] Harry is young.[(triple16)] @1: Harry is green.[(((triple14) -> rule3) OR ((((triple16) -> rule1)) -> rule3))] @2: Harry is smart.[(((((triple14) -> rule3) triple16) -> rule2) OR ((((((triple16) -> rule1)) -> rule3) triple16) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple1) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
Anne is smart.
("Anne" "is" "smart" "+")
triple6
((triple2 triple7) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple1) -> (rule3 % int2)) triple7) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
triple7
Charlie is blue.
("Charlie" "is" "blue" "+")
triple8
Charlie is green.
("Charlie" "is" "green" "+")
triple9
((triple8) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple10
Charlie is red.
("Charlie" "is" "red" "+")
triple11
Charlie is smart.
("Charlie" "is" "smart" "+")
triple12
((triple9 triple13) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple8) -> (rule3 % int2)) triple13) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
triple13
Harry is blue.
("Harry" "is" "blue" "+")
triple14
((triple16) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16
Harry is green.
("Harry" "is" "green" "+")
((triple14) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple16) -> (rule1 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((triple14) -> (rule3 % int2)) triple16) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((((triple16) -> (rule1 % int3))) -> (rule3 % int2)) triple16) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3