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