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