Bob is not red. Charlie is rough. Gary is red. Young, quiet things are big. If Charlie is red then Charlie is young. If something is rough then it is smart. If something is kind and quiet then it is smart. Red things are smart. If Gary is kind then Gary is not big. If something is kind then it is not quiet. Quiet things are kind.
Bob is not red.
("Bob" "is" "red" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Gary is red.
("Gary" "is" "red" "+")
Young, quiet things are big.
((("something" "is" "young" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If Charlie is red then Charlie is young.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "young" "+"))
If something is rough then it is smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If something is kind and quiet then it is smart.
((("something" "is" "kind" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
Red things are smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
If Gary is kind then Gary is not big.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "big" "-"))
If something is kind then it is not quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "-"))
Quiet things are kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
Charlie is rough.
True
1
proof
[(triple2)]
("Charlie" "is" "rough" "+")
triple2
Charlie is not rough.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "rough" "-")
triple2
Charlie is smart.
True
2
proof
[(((triple2) -> rule3))]
("Charlie" "is" "smart" "+")
((triple2) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is not smart.
False
2
inv-proof
[(((triple2) -> rule3))]
("Charlie" "is" "smart" "-")
((triple2) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "big" "-")
Bob is kind.
Unknown
rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "kind" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Bob is not red.[(triple1)] Charlie is rough.[(triple2)] Gary is red.[(triple3)] @1: Charlie is smart.[(((triple2) -> rule3))] Gary is smart.[(((triple3) -> rule5))]
Bob is not red.
("Bob" "is" "red" "-")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Gary is red.
("Gary" "is" "red" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple3) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1