Anne is nice. Anne is quiet. Anne is red. Anne is not smart. Dave is blue. Dave is red. Dave is rough. Gary is quiet. Gary is smart. Harry is not smart. Rough people are quiet. If Anne is smart and Anne is red then Anne is nice. If Anne is rough then Anne is nice. If Dave is smart and Dave is blue then Dave is nice. Blue, green people are not nice. If someone is green and not red then they are blue. All rough people are blue. All quiet people are green.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
Rough people are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
If Anne is smart and Anne is red then Anne is nice.
((("Anne" "is" "smart" "+") ("Anne" "is" "red" "+")) -> ("Anne" "is" "nice" "+"))
If Anne is rough then Anne is nice.
((("Anne" "is" "rough" "+")) -> ("Anne" "is" "nice" "+"))
If Dave is smart and Dave is blue then Dave is nice.
((("Dave" "is" "smart" "+") ("Dave" "is" "blue" "+")) -> ("Dave" "is" "nice" "+"))
Blue, green people are not nice.
((("someone" "is" "blue" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "nice" "-"))
If someone is green and not red then they are blue.
((("someone" "is" "green" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "blue" "+"))
All rough people are blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
All quiet people are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
Anne is red.
True
1
proof
[(triple3)]
("Anne" "is" "red" "+")
triple3
Dave is not rough.
False
1
inv-proof
[(triple7)]
("Dave" "is" "rough" "-")
triple7
Gary is green.
True
2
proof
[(((triple8) -> rule8))]
("Gary" "is" "green" "+")
((triple8) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not green.
False
2
inv-proof
[(((triple8) -> rule8))]
("Gary" "is" "green" "-")
((triple8) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Dave is green.
True
3
proof
[(((((triple7) -> rule1)) -> rule8))]
("Dave" "is" "green" "+")
((((triple7) -> (rule1 % int2))) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not green.
False
3
inv-proof
[(((((triple7) -> rule1)) -> rule8))]
("Dave" "is" "green" "-")
((((triple7) -> (rule1 % int2))) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not nice.
True
5
proof
[(((triple5 ((((triple7) -> rule1)) -> rule8)) -> rule5) OR ((((triple7) -> rule7) ((((triple7) -> rule1)) -> rule8)) -> rule5))]
("Dave" "is" "nice" "-")
((triple5 ((((triple7) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((triple7) -> (rule7 % int4)) ((((triple7) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is nice.
False
5
inv-proof
[(((triple5 ((((triple7) -> rule1)) -> rule8)) -> rule5) OR ((((triple7) -> rule7) ((((triple7) -> rule1)) -> rule8)) -> rule5))]
("Dave" "is" "nice" "+")
((triple5 ((((triple7) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((triple7) -> (rule7 % int4)) ((((triple7) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "blue" "-")
Gary is blue.
Unknown
rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "blue" "+")
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "blue" "-")
Harry is quiet.
Unknown
rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "quiet" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Anne is nice.[(triple1)] Anne is not smart.[(triple4)] Anne is quiet.[(triple2)] Anne is red.[(triple3)] Dave is blue.[(triple5 OR ((triple7) -> rule7))] Dave is red.[(triple6)] Dave is rough.[(triple7)] Gary is quiet.[(triple8)] Gary is smart.[(triple9)] Harry is not smart.[(triple10)] @1: Anne is green.[(((triple2) -> rule8))] Dave is quiet.[(((triple7) -> rule1))] Gary is green.[(((triple8) -> rule8))] @2: Dave is green.[(((((triple7) -> rule1)) -> rule8))] @3: Dave is not nice.[(((triple5 ((((triple7) -> rule1)) -> rule8)) -> rule5) OR ((((triple7) -> rule7) ((((triple7) -> rule1)) -> rule8)) -> rule5))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is not smart.
("Anne" "is" "smart" "-")
triple4
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
triple5
((triple7) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple6
Dave is rough.
("Dave" "is" "rough" "+")
triple7
Gary is quiet.
("Gary" "is" "quiet" "+")
triple8
Gary is smart.
("Gary" "is" "smart" "+")
triple9
Harry is not smart.
("Harry" "is" "smart" "-")
triple10
Anne is green.
("Anne" "is" "green" "+")
((triple2) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple7) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple8) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((((triple7) -> (rule1 % int2))) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
((triple5 ((((triple7) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((triple7) -> (rule7 % int4)) ((((triple7) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4