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