Charlie is green. Fiona is round. Gary is not young. Harry is big. Smart people are nice. If someone is white then they are nice. If someone is nice and young then they are smart. Big people are smart. If Gary is young then Gary is not nice. All nice, smart people are round. If Harry is nice and Harry is not white then Harry is big. All white, smart people are big.
Charlie is green.
("Charlie" "is" "green" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Gary is not young.
("Gary" "is" "young" "-")
Harry is big.
("Harry" "is" "big" "+")
Smart people are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
If someone is white then they are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice and young then they are smart.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
Big people are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
If Gary is young then Gary is not nice.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "nice" "-"))
All nice, smart people are round.
((("someone" "is" "nice" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
If Harry is nice and Harry is not white then Harry is big.
((("Harry" "is" "nice" "+") ("Harry" "is" "white" "~")) -> ("Harry" "is" "big" "+"))
All white, smart people are big.
((("someone" "is" "white" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
Harry is big.
True
1
proof
[(triple4)]
("Harry" "is" "big" "+")
triple4
Gary is young.
False
1
inv-proof
[(triple3)]
("Gary" "is" "young" "+")
triple3
Harry is smart.
True
2
proof
[(((triple4) -> rule4))]
("Harry" "is" "smart" "+")
((triple4) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not smart.
False
2
inv-proof
[(((triple4) -> rule4))]
("Harry" "is" "smart" "-")
((triple4) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "big" "-")
Gary is smart.
Unknown
rconc
[@2: Gary is smart.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("Gary" "is" "smart" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
@0: Charlie is green.[(triple1)] Fiona is round.[(triple2)] Gary is not young.[(triple3)] Harry is big.[(triple4)] @1: Harry is smart.[(((triple4) -> rule4))] @2: Harry is nice.[(((((triple4) -> rule4)) -> rule1))] @3: Harry is round.[(((((((triple4) -> rule4)) -> rule1) ((triple4) -> rule4)) -> rule6))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Fiona is round.
("Fiona" "is" "round" "+")
triple2
Gary is not young.
("Gary" "is" "young" "-")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
Harry is smart.
("Harry" "is" "smart" "+")
((triple4) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((((triple4) -> (rule4 % int3))) -> (rule1 % int2)) ((triple4) -> (rule4 % int3))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3