Bob is rough. Charlie is green. Dave is rough. Gary is nice. If something is smart then it is nice. If something is cold then it is nice. Rough, green things are nice. All smart things are quiet. All nice, green things are quiet. All rough things are not smart. If Bob is not kind then Bob is not smart. If something is green then it is rough.
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is nice.
("Gary" "is" "nice" "+")
If something is smart then it is nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
If something is cold then it is nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Rough, green things are nice.
((("something" "is" "rough" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
All smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
All nice, green things are quiet.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
All rough things are not smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "-"))
If Bob is not kind then Bob is not smart.
((("Bob" "is" "kind" "~")) -> ("Bob" "is" "smart" "-"))
If something is green then it is rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Bob is rough.
True
1
proof
[(triple1)]
("Bob" "is" "rough" "+")
triple1
Gary is not nice.
False
1
inv-proof
[(triple4)]
("Gary" "is" "nice" "-")
triple4
Bob is not smart.
True
2
proof
[(((triple1) -> rule6))]
("Bob" "is" "smart" "-")
((triple1) -> (rule6 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Dave is smart.
False
2
inv-proof
[(((triple3) -> rule6))]
("Dave" "is" "smart" "+")
((triple3) -> (rule6 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Charlie is not smart.
True
3
proof
[(((((triple2) -> rule8)) -> rule6))]
("Charlie" "is" "smart" "-")
((((triple2) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is smart.
False
3
inv-proof
[(((((triple2) -> rule8)) -> rule6))]
("Charlie" "is" "smart" "+")
((((triple2) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is quiet.
True
6
proof
[(((((((triple2) -> rule8) triple2) -> rule3) triple2) -> rule5))]
("Charlie" "is" "quiet" "+")
((((((triple2) -> (rule8 % int3)) triple2) -> (rule3 % int2)) triple2) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is not quiet.
False
6
inv-proof
[(((((((triple2) -> rule8) triple2) -> rule3) triple2) -> rule5))]
("Charlie" "is" "quiet" "-")
((((((triple2) -> (rule8 % int3)) triple2) -> (rule3 % int2)) triple2) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "nice" "+")
Gary is not rough.
Unknown
inv-rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "rough" "-")
Dave is quiet.
Unknown
rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "quiet" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Bob is rough.[(triple1)] Charlie is green.[(triple2)] Dave is rough.[(triple3)] Gary is nice.[(triple4)] @1: Bob is not smart.[(((triple1) -> rule6))] Charlie is rough.[(((triple2) -> rule8))] Dave is not smart.[(((triple3) -> rule6))] @2: Charlie is nice.[(((((triple2) -> rule8) triple2) -> rule3))] Charlie is not smart.[(((((triple2) -> rule8)) -> rule6))] @3: Charlie is quiet.[(((((((triple2) -> rule8) triple2) -> rule3) triple2) -> rule5))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Gary is nice.
("Gary" "is" "nice" "+")
triple4
Bob is not smart.
("Bob" "is" "smart" "-")
((triple1) -> (rule6 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple2) -> (rule8 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Dave is not smart.
("Dave" "is" "smart" "-")
((triple3) -> (rule6 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple2) -> (rule8 % int2)) triple2) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not smart.
("Charlie" "is" "smart" "-")
((((triple2) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((((triple2) -> (rule8 % int3)) triple2) -> (rule3 % int2)) triple2) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3