Anne is quiet. Anne is red. Anne is round. Erin is big. Erin is kind. Erin is red. Erin is rough. Erin is round. Erin is young. Fiona is kind. Harry is big. Harry is kind. Harry is red. Harry is round. Harry is young. If something is rough then it is young. All quiet, big things are kind. Young things are round. If something is kind then it is young. All quiet, red things are kind. If Harry is big and Harry is rough then Harry is red. If Harry is round and Harry is rough then Harry is red. If Erin is rough then Erin is big.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is rough then it is young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
All quiet, big things are kind.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
Young things are round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
If something is kind then it is young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
All quiet, red things are kind.
((("something" "is" "quiet" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If Harry is big and Harry is rough then Harry is red.
((("Harry" "is" "big" "+") ("Harry" "is" "rough" "+")) -> ("Harry" "is" "red" "+"))
If Harry is round and Harry is rough then Harry is red.
((("Harry" "is" "round" "+") ("Harry" "is" "rough" "+")) -> ("Harry" "is" "red" "+"))
If Erin is rough then Erin is big.
((("Erin" "is" "rough" "+")) -> ("Erin" "is" "big" "+"))
Harry is round.
True
1
proof
[(triple14 OR ((triple15) -> rule3) OR ((((triple12) -> rule4)) -> rule3))]
("Harry" "is" "round" "+")
triple14
((triple15) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple12) -> (rule4 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Anne is not red.
False
1
inv-proof
[(triple2)]
("Anne" "is" "red" "-")
triple2
Anne is kind.
True
3
proof
[(((triple1 triple2) -> rule5))]
("Anne" "is" "kind" "+")
((triple1 triple2) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Fiona is not young.
False
2
inv-proof
[(((triple10) -> rule4))]
("Fiona" "is" "young" "-")
((triple10) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is round.
True
3
proof
[(((((triple10) -> rule4)) -> rule3))]
("Fiona" "is" "round" "+")
((((triple10) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Anne is not young.
False
4
inv-proof
[(((((triple1 triple2) -> rule5)) -> rule4))]
("Anne" "is" "young" "-")
((((triple1 triple2) -> (rule5 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Anne is quiet.[(triple1)] Anne is red.[(triple2)] Anne is round.[(triple3 OR ((((((triple1 triple2) -> rule5)) -> rule4)) -> rule3))] Erin is big.[(triple4 OR ((triple7) -> rule8))] Erin is kind.[(triple5)] Erin is red.[(triple6)] Erin is rough.[(triple7)] Erin is round.[(triple8 OR ((triple9) -> rule3) OR ((((triple5) -> rule4)) -> rule3) OR ((((triple7) -> rule1)) -> rule3))] Erin is young.[(triple9 OR ((triple5) -> rule4) OR ((triple7) -> rule1))] Fiona is kind.[(triple10)] Harry is big.[(triple11)] Harry is kind.[(triple12)] Harry is red.[(triple13)] Harry is round.[(triple14 OR ((triple15) -> rule3) OR ((((triple12) -> rule4)) -> rule3))] Harry is young.[(triple15 OR ((triple12) -> rule4))] @1: Anne is kind.[(((triple1 triple2) -> rule5))] Fiona is young.[(((triple10) -> rule4))] @2: Anne is young.[(((((triple1 triple2) -> rule5)) -> rule4))] Fiona is round.[(((((triple10) -> rule4)) -> rule3))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
((((((triple1 triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
triple4
((triple7) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple5
Erin is red.
("Erin" "is" "red" "+")
triple6
Erin is rough.
("Erin" "is" "rough" "+")
triple7
Erin is round.
("Erin" "is" "round" "+")
triple8
((triple9) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple9
((triple5) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((triple7) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple10
Harry is big.
("Harry" "is" "big" "+")
triple11
Harry is kind.
("Harry" "is" "kind" "+")
triple12
Harry is red.
("Harry" "is" "red" "+")
triple13
Harry is round.
("Harry" "is" "round" "+")
triple14
((triple15) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple12) -> (rule4 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
triple15
((triple12) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((triple1 triple2) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple10) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple1 triple2) -> (rule5 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
((((triple10) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2