Bob is big. Bob is round. Charlie is not big. Charlie is young. Dave is blue. Dave is quiet. Erin is not quiet. If someone is big then they are not white. If someone is blue and not white then they are quiet. If someone is kind and not big then they are round. Young, blue people are kind. All young people are kind. If someone is white and not quiet then they are young.
Bob is big.
("Bob" "is" "big" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is not big.
("Charlie" "is" "big" "-")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is not quiet.
("Erin" "is" "quiet" "-")
If someone is big then they are not white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "-"))
If someone is blue and not white then they are quiet.
((("someone" "is" "blue" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "quiet" "+"))
If someone is kind and not big then they are round.
((("someone" "is" "kind" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "round" "+"))
Young, blue people are kind.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
All young people are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
If someone is white and not quiet then they are young.
((("someone" "is" "white" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "young" "+"))
Dave is blue.
True
1
proof
[(triple5)]
("Dave" "is" "blue" "+")
triple5
Dave is not blue.
False
1
inv-proof
[(triple5)]
("Dave" "is" "blue" "-")
triple5
Bob is not white.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "white" "-")
((triple1) -> (rule1 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is white.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "white" "+")
((triple1) -> (rule1 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Charlie is round.
True
4
proof
[(((((triple4) -> rule5) triple3) -> rule3))]
("Charlie" "is" "round" "+")
((((triple4) -> (rule5 % int2)) triple3) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not round.
False
4
inv-proof
[(((((triple4) -> rule5) triple3) -> rule3))]
("Charlie" "is" "round" "-")
((((triple4) -> (rule5 % int2)) triple3) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Erin is round.
Unknown
rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "round" "+")
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "quiet" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Bob is big.[(triple1)] Bob is round.[(triple2)] Charlie is not big.[(triple3)] Charlie is young.[(triple4)] Dave is blue.[(triple5)] Dave is quiet.[(triple6)] Erin is not quiet.[(triple7)] @1: Bob is not white.[(((triple1) -> rule1))] Charlie is kind.[(((triple4) -> rule5))] @2: Charlie is round.[(((((triple4) -> rule5) triple3) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Charlie is not big.
("Charlie" "is" "big" "-")
triple3
Charlie is young.
("Charlie" "is" "young" "+")
triple4
Dave is blue.
("Dave" "is" "blue" "+")
triple5
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
Erin is not quiet.
("Erin" "is" "quiet" "-")
triple7
Bob is not white.
("Bob" "is" "white" "-")
((triple1) -> (rule1 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple4) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((((triple4) -> (rule5 % int2)) triple3) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2