Anne is big. Anne is green. Anne is smart. Bob is big. Bob is white. Dave is white. Dave is young. Harry is big. Harry is green. Harry is round. Harry is smart. Harry is not white. If someone is green and big then they are round. All round people are big. If someone is kind and smart then they are big. If Harry is smart then Harry is round. White, smart people are green. If Bob is green and Bob is not kind then Bob is not white. All white people are smart. If Dave is smart and Dave is green then Dave is kind.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is not white.
("Harry" "is" "white" "-")
If someone is green and big then they are round.
((("someone" "is" "green" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
All round people are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If someone is kind and smart then they are big.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
If Harry is smart then Harry is round.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "round" "+"))
White, smart people are green.
((("someone" "is" "white" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If Bob is green and Bob is not kind then Bob is not white.
((("Bob" "is" "green" "+") ("Bob" "is" "kind" "~")) -> ("Bob" "is" "white" "-"))
All white people are smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
If Dave is smart and Dave is green then Dave is kind.
((("Dave" "is" "smart" "+") ("Dave" "is" "green" "+")) -> ("Dave" "is" "kind" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Bob is smart.
True
2
proof
[(((triple5) -> rule7))]
("Bob" "is" "smart" "+")
((triple5) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not smart.
False
2
inv-proof
[(((triple5) -> rule7))]
("Bob" "is" "smart" "-")
((triple5) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is green.
True
4
proof
[(((triple5 ((triple5) -> rule7)) -> rule5))]
("Bob" "is" "green" "+")
((triple5 ((triple5) -> (rule7 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not green.
False
4
inv-proof
[(((triple5 ((triple5) -> rule7)) -> rule5))]
("Bob" "is" "green" "-")
((triple5 ((triple5) -> (rule7 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is round.
True
6
proof
[(((((triple5 ((triple5) -> rule7)) -> rule5) triple4) -> rule1))]
("Bob" "is" "round" "+")
((((triple5 ((triple5) -> (rule7 % int3))) -> (rule5 % int2)) triple4) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Dave is not kind.
False
7
inv-proof
[(((((triple6) -> rule7) ((triple6 ((triple6) -> rule7)) -> rule5)) -> rule8))]
("Dave" "is" "kind" "-")
((((triple6) -> (rule7 % int3)) ((triple6 ((triple6) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is big.
True
10
proof
[(((((((triple6) -> rule7) ((triple6 ((triple6) -> rule7)) -> rule5)) -> rule8) ((triple6) -> rule7)) -> rule3))]
("Dave" "is" "big" "+")
((((((triple6) -> (rule7 % int4)) ((triple6 ((triple6) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule8 % int2)) ((triple6) -> (rule7 % int4))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is not big.
False
10
inv-proof
[(((((((triple6) -> rule7) ((triple6 ((triple6) -> rule7)) -> rule5)) -> rule8) ((triple6) -> rule7)) -> rule3))]
("Dave" "is" "big" "-")
((((((triple6) -> (rule7 % int4)) ((triple6 ((triple6) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule8 % int2)) ((triple6) -> (rule7 % int4))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is round.
True
15
proof
[(((((triple6 ((triple6) -> rule7)) -> rule5) ((((((triple6) -> rule7) ((triple6 ((triple6) -> rule7)) -> rule5)) -> rule8) ((triple6) -> rule7)) -> rule3)) -> rule1))]
("Dave" "is" "round" "+")
((((triple6 ((triple6) -> (rule7 % int5))) -> (rule5 % int4)) ((((((triple6) -> (rule7 % int5)) ((triple6 ((triple6) -> (rule7 % int5))) -> (rule5 % int4))) -> (rule8 % int3)) ((triple6) -> (rule7 % int5))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
int5
Dave is not round.
False
15
inv-proof
[(((((triple6 ((triple6) -> rule7)) -> rule5) ((((((triple6) -> rule7) ((triple6 ((triple6) -> rule7)) -> rule5)) -> rule8) ((triple6) -> rule7)) -> rule3)) -> rule1))]
("Dave" "is" "round" "-")
((((triple6 ((triple6) -> (rule7 % int5))) -> (rule5 % int4)) ((((((triple6) -> (rule7 % int5)) ((triple6 ((triple6) -> (rule7 % int5))) -> (rule5 % int4))) -> (rule8 % int3)) ((triple6) -> (rule7 % int5))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
int5
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Anne is big.[(triple1)] Anne is green.[(triple2)] Anne is smart.[(triple3)] Bob is big.[(triple4)] Bob is white.[(triple5)] Dave is white.[(triple6)] Dave is young.[(triple7)] Harry is big.[(triple8 OR ((triple10) -> rule2) OR ((((triple11) -> rule4)) -> rule2))] Harry is green.[(triple9)] Harry is not white.[(triple12)] Harry is round.[(triple10 OR ((triple11) -> rule4) OR ((triple9 triple8) -> rule1))] Harry is smart.[(triple11)] @1: Anne is round.[(((triple2 triple1) -> rule1))] Bob is smart.[(((triple5) -> rule7))] Dave is smart.[(((triple6) -> rule7))] @2: Bob is green.[(((triple5 ((triple5) -> rule7)) -> rule5))] Dave is green.[(((triple6 ((triple6) -> rule7)) -> rule5))] @3: Bob is round.[(((((triple5 ((triple5) -> rule7)) -> rule5) triple4) -> rule1))] Dave is kind.[(((((triple6) -> rule7) ((triple6 ((triple6) -> rule7)) -> rule5)) -> rule8))] @4: Dave is big.[(((((((triple6) -> rule7) ((triple6 ((triple6) -> rule7)) -> rule5)) -> rule8) ((triple6) -> rule7)) -> rule3))] @5: Dave is round.[(((((triple6 ((triple6) -> rule7)) -> rule5) ((((((triple6) -> rule7) ((triple6 ((triple6) -> rule7)) -> rule5)) -> rule8) ((triple6) -> rule7)) -> rule3)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Bob is big.
("Bob" "is" "big" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
((triple10) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((((triple11) -> (rule4 % int2))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
triple9
Harry is not white.
("Harry" "is" "white" "-")
triple12
Harry is round.
("Harry" "is" "round" "+")
triple10
((triple11) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((triple9 triple8) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple11
Anne is round.
("Anne" "is" "round" "+")
((triple2 triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple5) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple6) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple5 ((triple5) -> (rule7 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((triple6 ((triple6) -> (rule7 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((((triple5 ((triple5) -> (rule7 % int3))) -> (rule5 % int2)) triple4) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
((((triple6) -> (rule7 % int3)) ((triple6 ((triple6) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
((((((triple6) -> (rule7 % int4)) ((triple6 ((triple6) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule8 % int2)) ((triple6) -> (rule7 % int4))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
((((triple6 ((triple6) -> (rule7 % int5))) -> (rule5 % int4)) ((((((triple6) -> (rule7 % int5)) ((triple6 ((triple6) -> (rule7 % int5))) -> (rule5 % int4))) -> (rule8 % int3)) ((triple6) -> (rule7 % int5))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
int5