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