Dave is quiet. Gary is cold. Harry is big. All quiet people are not big. If Harry is furry and Harry is cold then Harry is not big. All cold people are round. If someone is cold and not big then they are young. If someone is quiet and rough then they are young. If someone is quiet and not big then they are not young.
Dave is quiet.
("Dave" "is" "quiet" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Harry is big.
("Harry" "is" "big" "+")
All quiet people are not big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "-"))
If Harry is furry and Harry is cold then Harry is not big.
((("Harry" "is" "furry" "+") ("Harry" "is" "cold" "+")) -> ("Harry" "is" "big" "-"))
All cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If someone is cold and not big then they are young.
((("someone" "is" "cold" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "young" "+"))
If someone is quiet and rough then they are young.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If someone is quiet and not big then they are not young.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "young" "-"))
Harry is big.
True
1
proof
[(triple3)]
("Harry" "is" "big" "+")
triple3
Harry is not big.
False
1
inv-proof
[(triple3)]
("Harry" "is" "big" "-")
triple3
Gary is round.
True
2
proof
[(((triple2) -> rule3))]
("Gary" "is" "round" "+")
((triple2) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Dave is big.
False
2
inv-proof
[(((triple1) -> rule1))]
("Dave" "is" "big" "+")
((triple1) -> (rule1 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is not young.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule6))]
("Dave" "is" "young" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Dave is not big.
("Dave" "is" "big" "-")
int2
Dave is young.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule6))]
("Dave" "is" "young" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Dave is not big.
("Dave" "is" "big" "-")
int2
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "round" "-")
Harry is young.
Unknown
rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "young" "+")
Harry is not round.
Unknown
inv-rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "round" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Dave is quiet.[(triple1)] Gary is cold.[(triple2)] Harry is big.[(triple3)] @1: Dave is not big.[(((triple1) -> rule1))] Gary is round.[(((triple2) -> rule3))] @2: Dave is not young.[(((triple1 ((triple1) -> rule1)) -> rule6))]
Dave is quiet.
("Dave" "is" "quiet" "+")
triple1
Gary is cold.
("Gary" "is" "cold" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
Dave is not big.
("Dave" "is" "big" "-")
((triple1) -> (rule1 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple2) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Dave is not young.
("Dave" "is" "young" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Dave is not big.
("Dave" "is" "big" "-")
int2