Gary is red. Harry is young. All rough things are quiet. All white things are young. If something is smart and quiet then it is rough. White, smart things are rough. All young things are rough. All rough things are green. If something is rough and not red then it is smart. Green things are white.
Gary is red.
("Gary" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
All rough things are quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
All white things are young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
If something is smart and quiet then it is rough.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
White, smart things are rough.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
All young things are rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
All rough things are green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
If something is rough and not red then it is smart.
((("something" "is" "rough" "+") ("something" "is" "red" "~")) -> ("something" "is" "smart" "+"))
Green things are white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
Gary is red.
True
1
proof
[(triple1)]
("Gary" "is" "red" "+")
triple1
Harry is not young.
False
1
inv-proof
[(triple2)]
("Harry" "is" "young" "-")
triple2
Harry is rough.
True
2
proof
[(((triple2) -> rule5))]
("Harry" "is" "rough" "+")
((triple2) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not rough.
False
2
inv-proof
[(((triple2) -> rule5))]
("Harry" "is" "rough" "-")
((triple2) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
True
3
proof
[(((((triple2) -> rule5)) -> rule6))]
("Harry" "is" "green" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not quiet.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule1))]
("Harry" "is" "quiet" "-")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
True
4
proof
[(((((((triple2) -> rule5)) -> rule6)) -> rule8))]
("Harry" "is" "white" "+")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is not white.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule6)) -> rule8))]
("Harry" "is" "white" "-")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Gary is not quiet.
Unknown
inv-rconc
[@6: Gary is quiet.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule2 <- rule8 <- rule6 <- rule3 <- FAIL)]]
("Gary" "is" "quiet" "-")
Gary is young.
Unknown
rconc
[@5: Gary is young.[CWA. Example of deepest failure = (rule2 <- rule8 <- rule6 <- rule3 <- rule7 <- FAIL)]]
("Gary" "is" "young" "+")
Gary is not green.
Unknown
inv-rconc
[@4: Gary is green.[CWA. Example of deepest failure = (rule6 <- rule5 <- rule2 <- rule8 <- FAIL)]]
("Gary" "is" "green" "-")
Gary is white.
Unknown
rconc
[@4: Gary is white.[CWA. Example of deepest failure = (rule8 <- rule6 <- rule3 <- rule7 <- FAIL)]]
("Gary" "is" "white" "+")
@0: Gary is red.[(triple1)] Harry is young.[(triple2)] @1: Harry is rough.[(((triple2) -> rule5))] @2: Harry is green.[(((((triple2) -> rule5)) -> rule6))] Harry is quiet.[(((((triple2) -> rule5)) -> rule1))] @3: Harry is white.[(((((((triple2) -> rule5)) -> rule6)) -> rule8))]
Gary is red.
("Gary" "is" "red" "+")
triple1
Harry is young.
("Harry" "is" "young" "+")
triple2
Harry is rough.
("Harry" "is" "rough" "+")
((triple2) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3