Dave is big. Dave is kind. Dave is young. Erin is big. Erin is green. Erin is kind. Erin is quiet. Harry is green. Harry is kind. Harry is quiet. Harry is smart. Harry is white. Quiet things are green. Big, smart things are green. If Erin is white then Erin is green. If Erin is kind then Erin is big. If Harry is smart and Harry is not kind then Harry is not young. If something is young then it is quiet. If something is big and green then it is white. If something is green and not smart then it is not young.
Dave is big.
("Dave" "is" "big" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Quiet things are green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
Big, smart things are green.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If Erin is white then Erin is green.
((("Erin" "is" "white" "+")) -> ("Erin" "is" "green" "+"))
If Erin is kind then Erin is big.
((("Erin" "is" "kind" "+")) -> ("Erin" "is" "big" "+"))
If Harry is smart and Harry is not kind then Harry is not young.
((("Harry" "is" "smart" "+") ("Harry" "is" "kind" "~")) -> ("Harry" "is" "young" "-"))
If something is young then it is quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
If something is big and green then it is white.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If something is green and not smart then it is not young.
((("something" "is" "green" "+") ("something" "is" "smart" "~")) -> ("something" "is" "young" "-"))
Erin is kind.
True
1
proof
[(triple6)]
("Erin" "is" "kind" "+")
triple6
Erin is not green.
False
1
inv-proof
[(triple5 OR ((triple7) -> rule1))]
("Erin" "is" "green" "-")
triple5
((triple7) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is white.
True
3
proof
[(((triple4 triple5) -> rule7) OR ((triple4 ((triple7) -> rule1)) -> rule7) OR ((((triple6) -> rule4) triple5) -> rule7) OR ((((triple6) -> rule4) ((triple7) -> rule1)) -> rule7))]
("Erin" "is" "white" "+")
((triple4 triple5) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple4 ((triple7) -> (rule1 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple6) -> (rule4 % int2)) triple5) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple6) -> (rule4 % int3)) ((triple7) -> (rule1 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is not white.
False
3
inv-proof
[(((triple4 triple5) -> rule7) OR ((triple4 ((triple7) -> rule1)) -> rule7) OR ((((triple6) -> rule4) triple5) -> rule7) OR ((((triple6) -> rule4) ((triple7) -> rule1)) -> rule7))]
("Erin" "is" "white" "-")
((triple4 triple5) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple4 ((triple7) -> (rule1 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple6) -> (rule4 % int2)) triple5) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple6) -> (rule4 % int3)) ((triple7) -> (rule1 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Dave is green.
True
3
proof
[(((((triple3) -> rule6)) -> rule1))]
("Dave" "is" "green" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not green.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule1))]
("Dave" "is" "green" "-")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is white.
True
5
proof
[(((triple1 ((((triple3) -> rule6)) -> rule1)) -> rule7))]
("Dave" "is" "white" "+")
((triple1 ((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is not white.
False
5
inv-proof
[(((triple1 ((((triple3) -> rule6)) -> rule1)) -> rule7))]
("Dave" "is" "white" "-")
((triple1 ((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Dave is big.[(triple1)] Dave is kind.[(triple2)] Dave is young.[(triple3)] Erin is big.[(triple4 OR ((triple6) -> rule4))] Erin is green.[(triple5 OR ((triple7) -> rule1))] Erin is kind.[(triple6)] Erin is quiet.[(triple7)] Harry is green.[(triple8 OR ((triple10) -> rule1))] Harry is kind.[(triple9)] Harry is quiet.[(triple10)] Harry is smart.[(triple11)] Harry is white.[(triple12)] @1: Dave is quiet.[(((triple3) -> rule6))] Erin is white.[(((triple4 triple5) -> rule7) OR ((triple4 ((triple7) -> rule1)) -> rule7) OR ((((triple6) -> rule4) triple5) -> rule7) OR ((((triple6) -> rule4) ((triple7) -> rule1)) -> rule7))] @2: Dave is green.[(((((triple3) -> rule6)) -> rule1))] @3: Dave is white.[(((triple1 ((((triple3) -> rule6)) -> rule1)) -> rule7))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
((triple6) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple5
((triple7) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple6
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
Harry is green.
("Harry" "is" "green" "+")
triple8
((triple10) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple12
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple3) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple4 triple5) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple4 ((triple7) -> (rule1 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple6) -> (rule4 % int2)) triple5) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple6) -> (rule4 % int3)) ((triple7) -> (rule1 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((triple1 ((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3