Anne is quiet. Anne is young. Charlie is cold. Charlie is quiet. Charlie is young. Dave is blue. Dave is kind. Dave is red. Dave is rough. Dave is young. Harry is not blue. Harry is cold. Harry is quiet. Harry is red. Harry is rough. Harry is young. All quiet people are red. If someone is rough and kind then they are cold. Quiet people are cold. If Anne is rough and Anne is red then Anne is quiet. All young, blue people are quiet. If someone is young and rough then they are quiet. Cold, red people are rough. If Charlie is cold and Charlie is blue then Charlie is quiet.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is not blue.
("Harry" "is" "blue" "-")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is young.
("Harry" "is" "young" "+")
All quiet people are red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
If someone is rough and kind then they are cold.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Quiet people are cold.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
If Anne is rough and Anne is red then Anne is quiet.
((("Anne" "is" "rough" "+") ("Anne" "is" "red" "+")) -> ("Anne" "is" "quiet" "+"))
All young, blue people are quiet.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If someone is young and rough then they are quiet.
((("someone" "is" "young" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
Cold, red people are rough.
((("someone" "is" "cold" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If Charlie is cold and Charlie is blue then Charlie is quiet.
((("Charlie" "is" "cold" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "quiet" "+"))
Harry is rough.
True
1
proof
[(triple15 OR ((triple12 triple14) -> rule7) OR ((triple12 ((triple13) -> rule1)) -> rule7) OR ((((triple13) -> rule3) triple14) -> rule7) OR ((((triple13) -> rule3) ((triple13) -> rule1)) -> rule7))]
("Harry" "is" "rough" "+")
triple15
((triple12 triple14) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple12 ((triple13) -> (rule1 % int2))) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple13) -> (rule3 % int2)) triple14) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple13) -> (rule3 % int3)) ((triple13) -> (rule1 % int2))) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Charlie is not quiet.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "quiet" "-")
triple4
Anne is red.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "red" "+")
((triple1) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not cold.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "cold" "-")
((triple1) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is rough.
True
5
proof
[(((((triple1) -> rule3) ((triple1) -> rule1)) -> rule7))]
("Anne" "is" "rough" "+")
((((triple1) -> (rule3 % int3)) ((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Charlie is not rough.
False
4
inv-proof
[(((triple3 ((triple4) -> rule1)) -> rule7) OR ((((triple4) -> rule3) ((triple4) -> rule1)) -> rule7))]
("Charlie" "is" "rough" "-")
((triple3 ((triple4) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((triple4) -> (rule3 % int3)) ((triple4) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Anne is quiet.[(triple1)] Anne is young.[(triple2)] Charlie is cold.[(triple3 OR ((triple4) -> rule3))] Charlie is quiet.[(triple4)] Charlie is young.[(triple5)] Dave is blue.[(triple6)] Dave is kind.[(triple7)] Dave is red.[(triple8 OR ((((triple10 triple6) -> rule5)) -> rule1) OR ((((triple10 triple9) -> rule6)) -> rule1))] Dave is rough.[(triple9 OR ((((((triple10 triple6) -> rule5)) -> rule3) triple8) -> rule7) OR ((((((triple10 triple6) -> rule5)) -> rule3) ((((triple10 triple6) -> rule5)) -> rule1)) -> rule7))] Dave is young.[(triple10)] Harry is cold.[(triple12 OR ((triple13) -> rule3) OR ((((triple16 triple15) -> rule6)) -> rule3))] Harry is not blue.[(triple11)] Harry is quiet.[(triple13 OR ((triple16 triple15) -> rule6) OR ((triple16 ((triple12 triple14) -> rule7)) -> rule6))] Harry is red.[(triple14 OR ((triple13) -> rule1) OR ((((triple16 triple15) -> rule6)) -> rule1))] Harry is rough.[(triple15 OR ((triple12 triple14) -> rule7) OR ((triple12 ((triple13) -> rule1)) -> rule7) OR ((((triple13) -> rule3) triple14) -> rule7) OR ((((triple13) -> rule3) ((triple13) -> rule1)) -> rule7))] Harry is young.[(triple16)] @1: Anne is cold.[(((triple1) -> rule3))] Anne is red.[(((triple1) -> rule1))] Charlie is red.[(((triple4) -> rule1))] Dave is cold.[(((triple9 triple7) -> rule2) OR ((((triple10 triple6) -> rule5)) -> rule3) OR ((((triple10 triple9) -> rule6)) -> rule3))] Dave is quiet.[(((triple10 triple6) -> rule5) OR ((triple10 triple9) -> rule6))] @2: Anne is rough.[(((((triple1) -> rule3) ((triple1) -> rule1)) -> rule7))] Charlie is rough.[(((triple3 ((triple4) -> rule1)) -> rule7) OR ((((triple4) -> rule3) ((triple4) -> rule1)) -> rule7))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
((triple4) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Dave is blue.
("Dave" "is" "blue" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Dave is red.
("Dave" "is" "red" "+")
triple8
((((triple10 triple6) -> (rule5 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((triple10 triple9) -> (rule6 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
triple9
((((((triple10 triple6) -> (rule5 % int3))) -> (rule3 % int2)) triple8) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((((triple10 triple6) -> (rule5 % int4))) -> (rule3 % int3)) ((((triple10 triple6) -> (rule5 % int4))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
triple10
Harry is cold.
("Harry" "is" "cold" "+")
triple12
((triple13) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple16 triple15) -> (rule6 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not blue.
("Harry" "is" "blue" "-")
triple11
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
((triple16 triple15) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple16 ((triple12 triple14) -> (rule7 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
triple14
((triple13) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple16 triple15) -> (rule6 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
triple15
((triple12 triple14) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple12 ((triple13) -> (rule1 % int2))) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple13) -> (rule3 % int2)) triple14) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple13) -> (rule3 % int3)) ((triple13) -> (rule1 % int2))) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
triple16
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple4) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple9 triple7) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple10 triple6) -> (rule5 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((triple10 triple9) -> (rule6 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple10 triple6) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple10 triple9) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1) -> (rule3 % int3)) ((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple3 ((triple4) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((triple4) -> (rule3 % int3)) ((triple4) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3