Dave is green. Dave is quiet. Dave is not rough. Dave is round. Dave is white. Fiona is blue. Fiona is quiet. Fiona is not rough. Fiona is round. Fiona is white. Harry is rough. Harry is not round. If someone is blue then they are not rough. Rough people are not white. Quiet, rough people are green. If Fiona is quiet then Fiona is green. If someone is rough and not white then they are quiet. Rough people are quiet.
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is not rough.
("Fiona" "is" "rough" "-")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is not round.
("Harry" "is" "round" "-")
If someone is blue then they are not rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "-"))
Rough people are not white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "-"))
Quiet, rough people are green.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
If Fiona is quiet then Fiona is green.
((("Fiona" "is" "quiet" "+")) -> ("Fiona" "is" "green" "+"))
If someone is rough and not white then they are quiet.
((("someone" "is" "rough" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "quiet" "+"))
Rough people are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
Dave is not rough.
True
1
proof
[(triple3)]
("Dave" "is" "rough" "-")
triple3
Dave is not green.
False
1
inv-proof
[(triple1)]
("Dave" "is" "green" "-")
triple1
Harry is not white.
True
2
proof
[(((triple11) -> rule2))]
("Harry" "is" "white" "-")
((triple11) -> (rule2 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is white.
False
2
inv-proof
[(((triple11) -> rule2))]
("Harry" "is" "white" "+")
((triple11) -> (rule2 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is green.
True
4
proof
[(((((triple11) -> rule6) triple11) -> rule3) OR ((((triple11 ((triple11) -> rule2)) -> rule5) triple11) -> rule3))]
("Harry" "is" "green" "+")
((((triple11) -> (rule6 % int2)) triple11) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple11 ((triple11) -> (rule2 % int3))) -> (rule5 % int2)) triple11) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not white.
("Harry" "is" "white" "-")
int3
Harry is not green.
False
4
inv-proof
[(((((triple11) -> rule6) triple11) -> rule3) OR ((((triple11 ((triple11) -> rule2)) -> rule5) triple11) -> rule3))]
("Harry" "is" "green" "-")
((((triple11) -> (rule6 % int2)) triple11) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple11 ((triple11) -> (rule2 % int3))) -> (rule5 % int2)) triple11) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not white.
("Harry" "is" "white" "-")
int3
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
@0: Dave is green.[(triple1)] Dave is not rough.[(triple3)] Dave is quiet.[(triple2)] Dave is round.[(triple4)] Dave is white.[(triple5)] Fiona is blue.[(triple6)] Fiona is not rough.[(triple8 OR ((triple6) -> rule1))] Fiona is quiet.[(triple7)] Fiona is round.[(triple9)] Fiona is white.[(triple10)] Harry is not round.[(triple12)] Harry is rough.[(triple11)] @1: Fiona is green.[(((triple7) -> rule4))] Harry is not white.[(((triple11) -> rule2))] Harry is quiet.[(((triple11) -> rule6) OR ((triple11 ((triple11) -> rule2)) -> rule5))] @2: Harry is green.[(((((triple11) -> rule6) triple11) -> rule3) OR ((((triple11 ((triple11) -> rule2)) -> rule5) triple11) -> rule3))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Dave is not rough.
("Dave" "is" "rough" "-")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple5
Fiona is blue.
("Fiona" "is" "blue" "+")
triple6
Fiona is not rough.
("Fiona" "is" "rough" "-")
triple8
((triple6) -> (rule1 % int1))
Fiona is not rough.
("Fiona" "is" "rough" "-")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple7
Fiona is round.
("Fiona" "is" "round" "+")
triple9
Fiona is white.
("Fiona" "is" "white" "+")
triple10
Harry is not round.
("Harry" "is" "round" "-")
triple12
Harry is rough.
("Harry" "is" "rough" "+")
triple11
Fiona is green.
("Fiona" "is" "green" "+")
((triple7) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Harry is not white.
("Harry" "is" "white" "-")
((triple11) -> (rule2 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple11) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple11 ((triple11) -> (rule2 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not white.
("Harry" "is" "white" "-")
int2
Harry is green.
("Harry" "is" "green" "+")
((((triple11) -> (rule6 % int2)) triple11) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple11 ((triple11) -> (rule2 % int3))) -> (rule5 % int2)) triple11) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not white.
("Harry" "is" "white" "-")
int3