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