Bob is big. Charlie is quiet. Erin is big. Gary is red. All red, quiet people are big. If someone is quiet and big then they are kind. All red people are big. Rough people are quiet. If someone is red then they are quiet. All rough, furry people are big.
Bob is big.
("Bob" "is" "big" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Erin is big.
("Erin" "is" "big" "+")
Gary is red.
("Gary" "is" "red" "+")
All red, quiet people are big.
((("someone" "is" "red" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
If someone is quiet and big then they are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
All red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
Rough people are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
If someone is red then they are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
All rough, furry people are big.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
Gary is red.
True
1
proof
[(triple4)]
("Gary" "is" "red" "+")
triple4
Erin is not big.
False
1
inv-proof
[(triple3)]
("Erin" "is" "big" "-")
triple3
Gary is quiet.
True
2
proof
[(((triple4) -> rule5))]
("Gary" "is" "quiet" "+")
((triple4) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not quiet.
False
2
inv-proof
[(((triple4) -> rule5))]
("Gary" "is" "quiet" "-")
((triple4) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
True
5
proof
[(((((triple4) -> rule5) ((triple4) -> rule3)) -> rule2) OR ((((triple4) -> rule5) ((triple4 ((triple4) -> rule5)) -> rule1)) -> rule2))]
("Gary" "is" "kind" "+")
((((triple4) -> (rule5 % int3)) ((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((triple4) -> (rule5 % int3)) ((triple4 ((triple4) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is not kind.
False
5
inv-proof
[(((((triple4) -> rule5) ((triple4) -> rule3)) -> rule2) OR ((((triple4) -> rule5) ((triple4 ((triple4) -> rule5)) -> rule1)) -> rule2))]
("Gary" "is" "kind" "-")
((((triple4) -> (rule5 % int3)) ((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((triple4) -> (rule5 % int3)) ((triple4 ((triple4) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Bob is not kind.
Unknown
inv-rconc
[@2: Bob is kind.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Bob" "is" "kind" "-")
Charlie is kind.
Unknown
rconc
[@2: Charlie is kind.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Charlie" "is" "kind" "+")
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
@0: Bob is big.[(triple1)] Charlie is quiet.[(triple2)] Erin is big.[(triple3)] Gary is red.[(triple4)] @1: Gary is big.[(((triple4) -> rule3) OR ((triple4 ((triple4) -> rule5)) -> rule1))] Gary is quiet.[(((triple4) -> rule5))] @2: Gary is kind.[(((((triple4) -> rule5) ((triple4) -> rule3)) -> rule2) OR ((((triple4) -> rule5) ((triple4 ((triple4) -> rule5)) -> rule1)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
Gary is red.
("Gary" "is" "red" "+")
triple4
Gary is big.
("Gary" "is" "big" "+")
((triple4) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple4 ((triple4) -> (rule5 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple4) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((((triple4) -> (rule5 % int3)) ((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((triple4) -> (rule5 % int3)) ((triple4 ((triple4) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3