Erin is furry. Fiona is blue. Gary is blue. Harry is big. All white people are big. All young, white people are round. All furry, blue people are round. If Gary is blue and Gary is round then Gary is rough. White people are rough. If someone is round and rough then they are big. All blue people are round. Blue, young people are round.
Erin is furry.
("Erin" "is" "furry" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Harry is big.
("Harry" "is" "big" "+")
All white people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
All young, white people are round.
((("someone" "is" "young" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
All furry, blue people are round.
((("someone" "is" "furry" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If Gary is blue and Gary is round then Gary is rough.
((("Gary" "is" "blue" "+") ("Gary" "is" "round" "+")) -> ("Gary" "is" "rough" "+"))
White people are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
If someone is round and rough then they are big.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
All blue people are round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
Blue, young people are round.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
Gary is blue.
True
1
proof
[(triple3)]
("Gary" "is" "blue" "+")
triple3
Erin is not furry.
False
1
inv-proof
[(triple1)]
("Erin" "is" "furry" "-")
triple1
Fiona is round.
True
2
proof
[(((triple2) -> rule7))]
("Fiona" "is" "round" "+")
((triple2) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is not round.
False
2
inv-proof
[(((triple2) -> rule7))]
("Fiona" "is" "round" "-")
((triple2) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Gary is rough.
True
4
proof
[(((triple3 ((triple3) -> rule7)) -> rule4))]
("Gary" "is" "rough" "+")
((triple3 ((triple3) -> (rule7 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is not rough.
False
4
inv-proof
[(((triple3 ((triple3) -> rule7)) -> rule4))]
("Gary" "is" "rough" "-")
((triple3 ((triple3) -> (rule7 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "rough" "-")
Harry is round.
Unknown
rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "round" "+")
Erin is not big.
Unknown
inv-rconc
[@2: Erin is big.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Erin" "is" "big" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
@0: Erin is furry.[(triple1)] Fiona is blue.[(triple2)] Gary is blue.[(triple3)] Harry is big.[(triple4)] @1: Fiona is round.[(((triple2) -> rule7))] Gary is round.[(((triple3) -> rule7))] @2: Gary is rough.[(((triple3 ((triple3) -> rule7)) -> rule4))] @3: Gary is big.[(((((triple3) -> rule7) ((triple3 ((triple3) -> rule7)) -> rule4)) -> rule6))]
Erin is furry.
("Erin" "is" "furry" "+")
triple1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple2
Gary is blue.
("Gary" "is" "blue" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
Fiona is round.
("Fiona" "is" "round" "+")
((triple2) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple3) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple3 ((triple3) -> (rule7 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((((triple3) -> (rule7 % int3)) ((triple3 ((triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3