Bob is big. Bob is smart. Bob is white. Dave is big. Dave is smart. Dave is young. Fiona is big. Fiona is kind. Fiona is not red. Harry is kind. Harry is red. Harry is white. Kind, red people are green. If someone is big and not kind then they are green. All red people are smart.
Bob is big.
("Bob" "is" "big" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is not red.
("Fiona" "is" "red" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is white.
("Harry" "is" "white" "+")
Kind, red people are green.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
If someone is big and not kind then they are green.
((("someone" "is" "big" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "green" "+"))
All red people are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
Dave is smart.
True
1
proof
[(triple5)]
("Dave" "is" "smart" "+")
triple5
Harry is not red.
False
1
inv-proof
[(triple11)]
("Harry" "is" "red" "-")
triple11
Harry is green.
True
3
proof
[(((triple10 triple11) -> rule1))]
("Harry" "is" "green" "+")
((triple10 triple11) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
3
inv-proof
[(((triple10 triple11) -> rule1))]
("Harry" "is" "green" "-")
((triple10 triple11) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "green" "-")
Bob is green.
Unknown
rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "green" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is big.[(triple1)] Bob is smart.[(triple2)] Bob is white.[(triple3)] Dave is big.[(triple4)] Dave is smart.[(triple5)] Dave is young.[(triple6)] Fiona is big.[(triple7)] Fiona is kind.[(triple8)] Fiona is not red.[(triple9)] Harry is kind.[(triple10)] Harry is red.[(triple11)] Harry is white.[(triple12)] @1: Harry is green.[(((triple10 triple11) -> rule1))] Harry is smart.[(((triple11) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Dave is young.
("Dave" "is" "young" "+")
triple6
Fiona is big.
("Fiona" "is" "big" "+")
triple7
Fiona is kind.
("Fiona" "is" "kind" "+")
triple8
Fiona is not red.
("Fiona" "is" "red" "-")
triple9
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple12
Harry is green.
("Harry" "is" "green" "+")
((triple10 triple11) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple11) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1