Bob is big. Bob is rough. Bob is young. Erin is big. Erin is not rough. Fiona is kind. Fiona is not red. Harry is big. Harry is kind. Harry is quiet. Harry is red. Harry is young. If something is big and not red then it is not kind. Red things are nice. Nice things are not rough.
Bob is big.
("Bob" "is" "big" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is not rough.
("Erin" "is" "rough" "-")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is not red.
("Fiona" "is" "red" "-")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is big and not red then it is not kind.
((("something" "is" "big" "+") ("something" "is" "red" "~")) -> ("something" "is" "kind" "-"))
Red things are nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
Nice things are not rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "-"))
Bob is young.
True
1
proof
[(triple3)]
("Bob" "is" "young" "+")
triple3
Harry is not quiet.
False
1
inv-proof
[(triple10)]
("Harry" "is" "quiet" "-")
triple10
Harry is nice.
True
2
proof
[(((triple11) -> rule2))]
("Harry" "is" "nice" "+")
((triple11) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not nice.
False
2
inv-proof
[(((triple11) -> rule2))]
("Harry" "is" "nice" "-")
((triple11) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not rough.
True
3
proof
[(((((triple11) -> rule2)) -> rule3))]
("Harry" "is" "rough" "-")
((((triple11) -> (rule2 % int2))) -> (rule3 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is rough.
False
3
inv-proof
[(((((triple11) -> rule2)) -> rule3))]
("Harry" "is" "rough" "+")
((((triple11) -> (rule2 % int2))) -> (rule3 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Fiona is not nice.
Unknown
inv-rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "nice" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "nice" "+")
Erin is not nice.
Unknown
inv-rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "nice" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Bob is big.[(triple1)] Bob is rough.[(triple2)] Bob is young.[(triple3)] Erin is big.[(triple4)] Erin is not rough.[(triple5)] Fiona is kind.[(triple6)] Fiona is not red.[(triple7)] Harry is big.[(triple8)] Harry is kind.[(triple9)] Harry is quiet.[(triple10)] Harry is red.[(triple11)] Harry is young.[(triple12)] @1: Harry is nice.[(((triple11) -> rule2))] @2: Harry is not rough.[(((((triple11) -> rule2)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
Erin is not rough.
("Erin" "is" "rough" "-")
triple5
Fiona is kind.
("Fiona" "is" "kind" "+")
triple6
Fiona is not red.
("Fiona" "is" "red" "-")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Harry is nice.
("Harry" "is" "nice" "+")
((triple11) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not rough.
("Harry" "is" "rough" "-")
((((triple11) -> (rule2 % int2))) -> (rule3 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2