Charlie is furry. Erin is not rough. Fiona is furry. Gary is big. Rough people are furry. If someone is rough then they are not white. Smart, big people are rough. Furry people are big. Big people are smart. If someone is rough and white then they are green. If Fiona is green then Fiona is white. If someone is white and not furry then they are not nice.
Charlie is furry.
("Charlie" "is" "furry" "+")
Erin is not rough.
("Erin" "is" "rough" "-")
Fiona is furry.
("Fiona" "is" "furry" "+")
Gary is big.
("Gary" "is" "big" "+")
Rough people are furry.
((("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
If someone is rough then they are not white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "-"))
Smart, big people are rough.
((("someone" "is" "smart" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
Furry people are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
Big people are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
If someone is rough and white then they are green.
((("someone" "is" "rough" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
If Fiona is green then Fiona is white.
((("Fiona" "is" "green" "+")) -> ("Fiona" "is" "white" "+"))
If someone is white and not furry then they are not nice.
((("someone" "is" "white" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "nice" "-"))
Erin is not rough.
True
1
proof
[(triple2)]
("Erin" "is" "rough" "-")
triple2
Fiona is not furry.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "furry" "-")
triple3
Gary is smart.
True
2
proof
[(((triple4) -> rule5))]
("Gary" "is" "smart" "+")
((triple4) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Fiona is not big.
False
2
inv-proof
[(((triple3) -> rule4))]
("Fiona" "is" "big" "-")
((triple3) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
True
3
proof
[(((((triple3) -> rule4)) -> rule5))]
("Fiona" "is" "smart" "+")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is not smart.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule5))]
("Fiona" "is" "smart" "-")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is rough.
True
6
proof
[(((((((triple3) -> rule4)) -> rule5) ((triple3) -> rule4)) -> rule3))]
("Fiona" "is" "rough" "+")
((((((triple3) -> (rule4 % int3))) -> (rule5 % int2)) ((triple3) -> (rule4 % int3))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Gary is not furry.
False
5
inv-proof
[(((((((triple4) -> rule5) triple4) -> rule3)) -> rule1))]
("Gary" "is" "furry" "-")
((((((triple4) -> (rule5 % int3)) triple4) -> (rule3 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Erin is not smart.
Unknown
inv-rconc
[@3: Erin is smart.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule1 <- FAIL)]]
("Erin" "is" "smart" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "green" "+")
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "green" "-")
Erin is big.
Unknown
rconc
[@2: Erin is big.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Erin" "is" "big" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Charlie is furry.[(triple1)] Erin is not rough.[(triple2)] Fiona is furry.[(triple3)] Gary is big.[(triple4)] @1: Charlie is big.[(((triple1) -> rule4))] Fiona is big.[(((triple3) -> rule4))] Gary is smart.[(((triple4) -> rule5))] @2: Charlie is smart.[(((((triple1) -> rule4)) -> rule5))] Fiona is smart.[(((((triple3) -> rule4)) -> rule5))] Gary is rough.[(((((triple4) -> rule5) triple4) -> rule3))] @3: Charlie is rough.[(((((((triple1) -> rule4)) -> rule5) ((triple1) -> rule4)) -> rule3))] Fiona is rough.[(((((((triple3) -> rule4)) -> rule5) ((triple3) -> rule4)) -> rule3))] Gary is furry.[(((((((triple4) -> rule5) triple4) -> rule3)) -> rule1))] Gary is not white.[(((((((triple4) -> rule5) triple4) -> rule3)) -> rule2))] @4: Charlie is not white.[(((((((((triple1) -> rule4)) -> rule5) ((triple1) -> rule4)) -> rule3)) -> rule2))] Fiona is not white.[(((((((((triple3) -> rule4)) -> rule5) ((triple3) -> rule4)) -> rule3)) -> rule2))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Erin is not rough.
("Erin" "is" "rough" "-")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
triple4
Charlie is big.
("Charlie" "is" "big" "+")
((triple1) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple3) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple4) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((((triple4) -> (rule5 % int2)) triple4) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2)) ((triple1) -> (rule4 % int3))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
((((((triple3) -> (rule4 % int3))) -> (rule5 % int2)) ((triple3) -> (rule4 % int3))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
((((((triple4) -> (rule5 % int3)) triple4) -> (rule3 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not white.
("Gary" "is" "white" "-")
((((((triple4) -> (rule5 % int3)) triple4) -> (rule3 % int2))) -> (rule2 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Charlie is not white.
("Charlie" "is" "white" "-")
((((((((triple1) -> (rule4 % int4))) -> (rule5 % int3)) ((triple1) -> (rule4 % int4))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is not white.
("Charlie" "is" "white" "-")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Fiona is not white.
("Fiona" "is" "white" "-")
((((((((triple3) -> (rule4 % int4))) -> (rule5 % int3)) ((triple3) -> (rule4 % int4))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is not white.
("Fiona" "is" "white" "-")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4