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