Bob is big. Bob is blue. Bob is white. Erin is not kind. Harry is big. Harry is kind. Harry is nice. Rough things are not blue. Kind, rough things are young. All blue things are young. All white, big things are not rough. If Harry is young then Harry is white. If Harry is nice then Harry is blue.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is white.
("Bob" "is" "white" "+")
Erin is not kind.
("Erin" "is" "kind" "-")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Rough things are not blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "-"))
Kind, rough things are young.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
All blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
All white, big things are not rough.
((("something" "is" "white" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "-"))
If Harry is young then Harry is white.
((("Harry" "is" "young" "+")) -> ("Harry" "is" "white" "+"))
If Harry is nice then Harry is blue.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "blue" "+"))
Bob is white.
True
1
proof
[(triple3)]
("Bob" "is" "white" "+")
triple3
Harry is not big.
False
1
inv-proof
[(triple5)]
("Harry" "is" "big" "-")
triple5
Harry is blue.
True
2
proof
[(((triple7) -> rule6))]
("Harry" "is" "blue" "+")
((triple7) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple7) -> rule6))]
("Harry" "is" "blue" "-")
((triple7) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
True
3
proof
[(((((triple7) -> rule6)) -> rule3))]
("Harry" "is" "young" "+")
((((triple7) -> (rule6 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not young.
False
3
inv-proof
[(((((triple7) -> rule6)) -> rule3))]
("Harry" "is" "young" "-")
((((triple7) -> (rule6 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Erin is not young.
Unknown
inv-rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "young" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Bob is big.[(triple1)] Bob is blue.[(triple2)] Bob is white.[(triple3)] Erin is not kind.[(triple4)] Harry is big.[(triple5)] Harry is kind.[(triple6)] Harry is nice.[(triple7)] @1: Bob is not rough.[(((triple3 triple1) -> rule4))] Bob is young.[(((triple2) -> rule3))] Harry is blue.[(((triple7) -> rule6))] @2: Harry is young.[(((((triple7) -> rule6)) -> rule3))] @3: Harry is white.[(((((((triple7) -> rule6)) -> rule3)) -> rule5))] @4: Harry is not rough.[(((((((((triple7) -> rule6)) -> rule3)) -> rule5) triple5) -> rule4))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Erin is not kind.
("Erin" "is" "kind" "-")
triple4
Harry is big.
("Harry" "is" "big" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is nice.
("Harry" "is" "nice" "+")
triple7
Bob is not rough.
("Bob" "is" "rough" "-")
((triple3 triple1) -> (rule4 % int1))
Bob is not rough.
("Bob" "is" "rough" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple2) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple7) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((((triple7) -> (rule6 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((((((triple7) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is not rough.
("Harry" "is" "rough" "-")
((((((((triple7) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) triple5) -> (rule4 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4