Dave is smart. Gary is round. Harry is not smart. If Dave is round then Dave is not quiet. If Harry is green and Harry is not quiet then Harry is cold. Blue people are round. If Harry is round then Harry is not big. If someone is smart then they are blue. If someone is blue and not round then they are not big.
Dave is smart.
("Dave" "is" "smart" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
If Dave is round then Dave is not quiet.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "quiet" "-"))
If Harry is green and Harry is not quiet then Harry is cold.
((("Harry" "is" "green" "+") ("Harry" "is" "quiet" "~")) -> ("Harry" "is" "cold" "+"))
Blue people are round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If Harry is round then Harry is not big.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "big" "-"))
If someone is smart then they are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue and not round then they are not big.
((("someone" "is" "blue" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "big" "-"))
Dave is smart.
True
1
proof
[(triple1)]
("Dave" "is" "smart" "+")
triple1
Harry is smart.
False
1
inv-proof
[(triple3)]
("Harry" "is" "smart" "+")
triple3
Dave is blue.
True
2
proof
[(((triple1) -> rule5))]
("Dave" "is" "blue" "+")
((triple1) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple1) -> rule5))]
("Dave" "is" "blue" "-")
((triple1) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
True
3
proof
[(((((triple1) -> rule5)) -> rule3))]
("Dave" "is" "round" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not round.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule3))]
("Dave" "is" "round" "-")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not quiet.
True
4
proof
[(((((((triple1) -> rule5)) -> rule3)) -> rule1))]
("Dave" "is" "quiet" "-")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is quiet.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule3)) -> rule1))]
("Dave" "is" "quiet" "+")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "blue" "-")
Harry is blue.
Unknown
rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "blue" "+")
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "cold" "-")
Harry is round.
Unknown
rconc
[@2: Harry is round.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Harry" "is" "round" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Dave is smart.[(triple1)] Gary is round.[(triple2)] Harry is not smart.[(triple3)] @1: Dave is blue.[(((triple1) -> rule5))] @2: Dave is round.[(((((triple1) -> rule5)) -> rule3))] @3: Dave is not quiet.[(((((((triple1) -> rule5)) -> rule3)) -> rule1))]
Dave is smart.
("Dave" "is" "smart" "+")
triple1
Gary is round.
("Gary" "is" "round" "+")
triple2
Harry is not smart.
("Harry" "is" "smart" "-")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
((triple1) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not quiet.
("Dave" "is" "quiet" "-")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3