Bob is not cold. Bob is rough. Dave is furry. Erin is cold. Erin is white. Harry is red. Harry is not rough. All white people are nice. If Harry is red and Harry is young then Harry is nice. If someone is rough then they are not young. All young people are white. All nice, white people are rough. If Bob is not young then Bob is not cold.
Bob is not cold.
("Bob" "is" "cold" "-")
Bob is rough.
("Bob" "is" "rough" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
All white people are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
If Harry is red and Harry is young then Harry is nice.
((("Harry" "is" "red" "+") ("Harry" "is" "young" "+")) -> ("Harry" "is" "nice" "+"))
If someone is rough then they are not young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "-"))
All young people are white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
All nice, white people are rough.
((("someone" "is" "nice" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
If Bob is not young then Bob is not cold.
((("Bob" "is" "young" "~")) -> ("Bob" "is" "cold" "-"))
Bob is not cold.
True
1
proof
[(triple1 OR ((((triple2) -> rule3)) -> rule6))]
("Bob" "is" "cold" "-")
triple1
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Bob is not young.
("Bob" "is" "young" "-")
int2
Erin is not cold.
False
1
inv-proof
[(triple4)]
("Erin" "is" "cold" "-")
triple4
Erin is nice.
True
2
proof
[(((triple5) -> rule1))]
("Erin" "is" "nice" "+")
((triple5) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not nice.
False
2
inv-proof
[(((triple5) -> rule1))]
("Erin" "is" "nice" "-")
((triple5) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
True
4
proof
[(((((triple5) -> rule1) triple5) -> rule5))]
("Erin" "is" "rough" "+")
((((triple5) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is not rough.
False
4
inv-proof
[(((((triple5) -> rule1) triple5) -> rule5))]
("Erin" "is" "rough" "-")
((((triple5) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is not young.
True
5
proof
[(((((((triple5) -> rule1) triple5) -> rule5)) -> rule3))]
("Erin" "is" "young" "-")
((((((triple5) -> (rule1 % int3)) triple5) -> (rule5 % int2))) -> (rule3 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is young.
False
5
inv-proof
[(((((((triple5) -> rule1) triple5) -> rule5)) -> rule3))]
("Erin" "is" "young" "+")
((((((triple5) -> (rule1 % int3)) triple5) -> (rule5 % int2))) -> (rule3 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Dave is not nice.
Unknown
inv-rconc
[@2: Dave is nice.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Dave" "is" "nice" "-")
Bob is nice.
Unknown
rconc
[@2: Bob is nice.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Bob" "is" "nice" "+")
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "white" "-")
Harry is white.
Unknown
rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "white" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Bob is not cold.[(triple1 OR ((((triple2) -> rule3)) -> rule6))] Bob is rough.[(triple2)] Dave is furry.[(triple3)] Erin is cold.[(triple4)] Erin is white.[(triple5)] Harry is not rough.[(triple7)] Harry is red.[(triple6)] @1: Bob is not young.[(((triple2) -> rule3))] Erin is nice.[(((triple5) -> rule1))] @2: Erin is rough.[(((((triple5) -> rule1) triple5) -> rule5))] @3: Erin is not young.[(((((((triple5) -> rule1) triple5) -> rule5)) -> rule3))]
Bob is not cold.
("Bob" "is" "cold" "-")
triple1
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Bob is not young.
("Bob" "is" "young" "-")
int2
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
triple4
Erin is white.
("Erin" "is" "white" "+")
triple5
Harry is not rough.
("Harry" "is" "rough" "-")
triple7
Harry is red.
("Harry" "is" "red" "+")
triple6
Bob is not young.
("Bob" "is" "young" "-")
((triple2) -> (rule3 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple5) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((((triple5) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is not young.
("Erin" "is" "young" "-")
((((((triple5) -> (rule1 % int3)) triple5) -> (rule5 % int2))) -> (rule3 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3