Bob is quiet. Bob is white. Bob is young. Charlie is rough. Erin is kind. Erin is young. Harry is young. Round, white things are rough. All kind, quiet things are young. All kind things are white. If Harry is young and Harry is kind then Harry is rough. All quiet things are rough. If something is rough then it is quiet. If Charlie is big and Charlie is round then Charlie is rough. All white things are big.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is young.
("Harry" "is" "young" "+")
Round, white things are rough.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
All kind, quiet things are young.
((("something" "is" "kind" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
All kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
If Harry is young and Harry is kind then Harry is rough.
((("Harry" "is" "young" "+") ("Harry" "is" "kind" "+")) -> ("Harry" "is" "rough" "+"))
All quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
If something is rough then it is quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
If Charlie is big and Charlie is round then Charlie is rough.
((("Charlie" "is" "big" "+") ("Charlie" "is" "round" "+")) -> ("Charlie" "is" "rough" "+"))
All white things are big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
Bob is white.
True
1
proof
[(triple2)]
("Bob" "is" "white" "+")
triple2
Erin is not young.
False
1
inv-proof
[(triple6)]
("Erin" "is" "young" "-")
triple6
Charlie is quiet.
True
2
proof
[(((triple4) -> rule6))]
("Charlie" "is" "quiet" "+")
((triple4) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Erin is not white.
False
2
inv-proof
[(((triple5) -> rule3))]
("Erin" "is" "white" "-")
((triple5) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is not quiet.
Unknown
inv-rconc
[@2: Erin is quiet.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Erin" "is" "quiet" "-")
Harry is big.
Unknown
rconc
[@2: Harry is big.[CWA. Example of deepest failure = (rule8 <- rule3 <- FAIL)]]
("Harry" "is" "big" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is quiet.[(triple1)] Bob is white.[(triple2)] Bob is young.[(triple3)] Charlie is rough.[(triple4)] Erin is kind.[(triple5)] Erin is young.[(triple6)] Harry is young.[(triple7)] @1: Bob is big.[(((triple2) -> rule8))] Bob is rough.[(((triple1) -> rule5))] Charlie is quiet.[(((triple4) -> rule6))] Erin is white.[(((triple5) -> rule3))] @2: Erin is big.[(((((triple5) -> rule3)) -> rule8))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
triple5
Erin is young.
("Erin" "is" "young" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Bob is big.
("Bob" "is" "big" "+")
((triple2) -> (rule8 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple4) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple5) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((((triple5) -> (rule3 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2