Bob is nice. Bob is red. Bob is smart. Dave is green. Dave is not nice. Dave is red. Dave is smart. Dave is young. Gary is red. Harry is cold. If something is young and white then it is cold. All white things are nice. Cold things are white. If Dave is smart then Dave is red. All nice things are smart. If Bob is cold then Bob is red.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is not nice.
("Dave" "is" "nice" "-")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is cold.
("Harry" "is" "cold" "+")
If something is young and white then it is cold.
((("something" "is" "young" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
All white things are nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
Cold things are white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
If Dave is smart then Dave is red.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "red" "+"))
All nice things are smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
If Bob is cold then Bob is red.
((("Bob" "is" "cold" "+")) -> ("Bob" "is" "red" "+"))
Bob is red.
True
1
proof
[(triple2)]
("Bob" "is" "red" "+")
triple2
Gary is not red.
False
1
inv-proof
[(triple9)]
("Gary" "is" "red" "-")
triple9
Harry is white.
True
2
proof
[(((triple10) -> rule3))]
("Harry" "is" "white" "+")
((triple10) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple10) -> rule3))]
("Harry" "is" "white" "-")
((triple10) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is nice.
True
3
proof
[(((((triple10) -> rule3)) -> rule2))]
("Harry" "is" "nice" "+")
((((triple10) -> (rule3 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not nice.
False
3
inv-proof
[(((((triple10) -> rule3)) -> rule2))]
("Harry" "is" "nice" "-")
((((triple10) -> (rule3 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is smart.
True
4
proof
[(((((((triple10) -> rule3)) -> rule2)) -> rule5))]
("Harry" "is" "smart" "+")
((((((triple10) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is not smart.
False
4
inv-proof
[(((((((triple10) -> rule3)) -> rule2)) -> rule5))]
("Harry" "is" "smart" "-")
((((((triple10) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Gary is not smart.
Unknown
inv-rconc
[@4: Gary is smart.[CWA. Example of deepest failure = (rule5 <- rule2 <- rule3 <- rule1 <- FAIL)]]
("Gary" "is" "smart" "-")
Bob is white.
Unknown
rconc
[@2: Bob is white.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Bob" "is" "white" "+")
Dave is not cold.
Unknown
inv-rconc
[@2: Dave is cold.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Dave" "is" "cold" "-")
Dave is white.
Unknown
rconc
[@2: Dave is white.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Dave" "is" "white" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Bob is nice.[(triple1)] Bob is red.[(triple2)] Bob is smart.[(triple3 OR ((triple1) -> rule5))] Dave is green.[(triple4)] Dave is not nice.[(triple5)] Dave is red.[(triple6 OR ((triple7) -> rule4))] Dave is smart.[(triple7)] Dave is young.[(triple8)] Gary is red.[(triple9)] Harry is cold.[(triple10)] @1: Harry is white.[(((triple10) -> rule3))] @2: Harry is nice.[(((((triple10) -> rule3)) -> rule2))] @3: Harry is smart.[(((((((triple10) -> rule3)) -> rule2)) -> rule5))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
((triple1) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple4
Dave is not nice.
("Dave" "is" "nice" "-")
triple5
Dave is red.
("Dave" "is" "red" "+")
triple6
((triple7) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple7
Dave is young.
("Dave" "is" "young" "+")
triple8
Gary is red.
("Gary" "is" "red" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Harry is white.
("Harry" "is" "white" "+")
((triple10) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((((triple10) -> (rule3 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((((triple10) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3