Anne is big. Gary is smart. Harry is big. All big, smart things are not rough. If Harry is big then Harry is blue. If Harry is not round then Harry is smart. If Anne is rough and Anne is not blue then Anne is round. All big things are smart. If Gary is round and Gary is rough then Gary is big.
Anne is big.
("Anne" "is" "big" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
All big, smart things are not rough.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "-"))
If Harry is big then Harry is blue.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "blue" "+"))
If Harry is not round then Harry is smart.
((("Harry" "is" "round" "~")) -> ("Harry" "is" "smart" "+"))
If Anne is rough and Anne is not blue then Anne is round.
((("Anne" "is" "rough" "+") ("Anne" "is" "blue" "~")) -> ("Anne" "is" "round" "+"))
All big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If Gary is round and Gary is rough then Gary is big.
((("Gary" "is" "round" "+") ("Gary" "is" "rough" "+")) -> ("Gary" "is" "big" "+"))
Gary is smart.
True
1
proof
[(triple2)]
("Gary" "is" "smart" "+")
triple2
Harry is not big.
False
1
inv-proof
[(triple3)]
("Harry" "is" "big" "-")
triple3
Harry is smart.
True
2
proof
[(((triple3) -> rule5))]
("Harry" "is" "smart" "+")
((triple3) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not smart.
False
2
inv-proof
[(((triple3) -> rule5))]
("Harry" "is" "smart" "-")
((triple3) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Anne is not rough.
True
4
proof
[(((triple1 ((triple1) -> rule5)) -> rule1))]
("Anne" "is" "rough" "-")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Anne is not rough.
("Anne" "is" "rough" "-")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Harry is rough.
False
4
inv-proof
[(((triple3 ((triple3) -> rule5)) -> rule1))]
("Harry" "is" "rough" "+")
((triple3 ((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Anne is not round.
Unknown
inv-rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "round" "-")
Gary is big.
Unknown
rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "big" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Anne is big.[(triple1)] Gary is smart.[(triple2)] Harry is big.[(triple3)] @1: Anne is smart.[(((triple1) -> rule5))] Harry is blue.[(((triple3) -> rule2))] Harry is smart.[(((triple3) -> rule5))] @2: Anne is not rough.[(((triple1 ((triple1) -> rule5)) -> rule1))] Harry is not rough.[(((triple3 ((triple3) -> rule5)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Gary is smart.
("Gary" "is" "smart" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple3) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Anne is not rough.
("Anne" "is" "rough" "-")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Anne is not rough.
("Anne" "is" "rough" "-")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Harry is not rough.
("Harry" "is" "rough" "-")
((triple3 ((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2