Charlie is green. Charlie is kind. Charlie is nice. Erin is not big. Erin is nice. Harry is kind. Harry is not nice. All furry, white people are kind. All rough people are kind. Nice, kind people are green. Rough people are not white. All kind people are big. If someone is big then they are rough.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Erin is not big.
("Erin" "is" "big" "-")
Erin is nice.
("Erin" "is" "nice" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is not nice.
("Harry" "is" "nice" "-")
All furry, white people are kind.
((("someone" "is" "furry" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
All rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
Nice, kind people are green.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
Rough people are not white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "-"))
All kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If someone is big then they are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
Erin is not big.
True
1
proof
[(triple4)]
("Erin" "is" "big" "-")
triple4
Charlie is not green.
False
1
inv-proof
[(triple1 OR ((triple3 triple2) -> rule3))]
("Charlie" "is" "green" "-")
triple1
((triple3 triple2) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is big.
True
2
proof
[(((triple2) -> rule5))]
("Charlie" "is" "big" "+")
((triple2) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple6) -> rule5))]
("Harry" "is" "big" "-")
((triple6) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Charlie is rough.
True
3
proof
[(((((triple2) -> rule5)) -> rule6))]
("Charlie" "is" "rough" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Harry is not rough.
False
3
inv-proof
[(((((triple6) -> rule5)) -> rule6))]
("Harry" "is" "rough" "-")
((((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not white.
True
4
proof
[(((((((triple6) -> rule5)) -> rule6)) -> rule4))]
("Harry" "is" "white" "-")
((((((triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Charlie is white.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule6)) -> rule4))]
("Charlie" "is" "white" "+")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is not white.
("Charlie" "is" "white" "-")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Erin is not green.
Unknown
inv-rconc
[@3: Erin is green.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule6 <- FAIL)]]
("Erin" "is" "green" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "green" "+")
Erin is not kind.
Unknown
inv-rconc
[@2: Erin is kind.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("Erin" "is" "kind" "-")
Erin is rough.
Unknown
rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "rough" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Charlie is green.[(triple1 OR ((triple3 triple2) -> rule3))] Charlie is kind.[(triple2)] Charlie is nice.[(triple3)] Erin is nice.[(triple5)] Erin is not big.[(triple4)] Harry is kind.[(triple6)] Harry is not nice.[(triple7)] @1: Charlie is big.[(((triple2) -> rule5))] Harry is big.[(((triple6) -> rule5))] @2: Charlie is rough.[(((((triple2) -> rule5)) -> rule6))] Harry is rough.[(((((triple6) -> rule5)) -> rule6))] @3: Charlie is not white.[(((((((triple2) -> rule5)) -> rule6)) -> rule4))] Harry is not white.[(((((((triple6) -> rule5)) -> rule6)) -> rule4))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
((triple3 triple2) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple5
Erin is not big.
("Erin" "is" "big" "-")
triple4
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is not nice.
("Harry" "is" "nice" "-")
triple7
Charlie is big.
("Charlie" "is" "big" "+")
((triple2) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple6) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Charlie is not white.
("Charlie" "is" "white" "-")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is not white.
("Charlie" "is" "white" "-")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Harry is not white.
("Harry" "is" "white" "-")
((((((triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3