Gary is round. All round people are young. If Gary is cold then Gary is not round. If someone is big then they are nice. All big people are not rough. Green, young people are rough. If someone is cold and not young then they are green. All young people are green. Big people are green.
Gary is round.
("Gary" "is" "round" "+")
All round people are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
If Gary is cold then Gary is not round.
((("Gary" "is" "cold" "+")) -> ("Gary" "is" "round" "-"))
If someone is big then they are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
All big people are not rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "-"))
Green, young people are rough.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If someone is cold and not young then they are green.
((("someone" "is" "cold" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "green" "+"))
All young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
Big people are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
Gary is round.
True
1
proof
[(triple1)]
("Gary" "is" "round" "+")
triple1
Gary is not round.
False
1
inv-proof
[(triple1)]
("Gary" "is" "round" "-")
triple1
Gary is young.
True
2
proof
[(((triple1) -> rule1))]
("Gary" "is" "young" "+")
((triple1) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not young.
False
2
inv-proof
[(((triple1) -> rule1))]
("Gary" "is" "young" "-")
((triple1) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
True
3
proof
[(((((triple1) -> rule1)) -> rule7))]
("Gary" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not green.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule7))]
("Gary" "is" "green" "-")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is rough.
True
6
proof
[(((((((triple1) -> rule1)) -> rule7) ((triple1) -> rule1)) -> rule5))]
("Gary" "is" "rough" "+")
((((((triple1) -> (rule1 % int3))) -> (rule7 % int2)) ((triple1) -> (rule1 % int3))) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is not rough.
False
6
inv-proof
[(((((((triple1) -> rule1)) -> rule7) ((triple1) -> rule1)) -> rule5))]
("Gary" "is" "rough" "-")
((((((triple1) -> (rule1 % int3))) -> (rule7 % int2)) ((triple1) -> (rule1 % int3))) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "nice" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Gary is round.[(triple1)] @1: Gary is young.[(((triple1) -> rule1))] @2: Gary is green.[(((((triple1) -> rule1)) -> rule7))] @3: Gary is rough.[(((((((triple1) -> rule1)) -> rule7) ((triple1) -> rule1)) -> rule5))]
Gary is round.
("Gary" "is" "round" "+")
triple1
Gary is young.
("Gary" "is" "young" "+")
((triple1) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((((((triple1) -> (rule1 % int3))) -> (rule7 % int2)) ((triple1) -> (rule1 % int3))) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3