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