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