Bob is kind. Dave is kind. Fiona is not blue. Harry is kind. Green people are young. If Harry is blue then Harry is nice. If Fiona is nice and Fiona is not blue then Fiona is green. All green people are nice. All young people are green. Green people are not white. If Bob is kind then Bob is young. If Fiona is not young and Fiona is not blue then Fiona is not white.
Bob is kind.
("Bob" "is" "kind" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Fiona is not blue.
("Fiona" "is" "blue" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Green people are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If Harry is blue then Harry is nice.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "nice" "+"))
If Fiona is nice and Fiona is not blue then Fiona is green.
((("Fiona" "is" "nice" "+") ("Fiona" "is" "blue" "~")) -> ("Fiona" "is" "green" "+"))
All green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
All young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
Green people are not white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "-"))
If Bob is kind then Bob is young.
((("Bob" "is" "kind" "+")) -> ("Bob" "is" "young" "+"))
If Fiona is not young and Fiona is not blue then Fiona is not white.
((("Fiona" "is" "young" "~") ("Fiona" "is" "blue" "~")) -> ("Fiona" "is" "white" "-"))
Bob is kind.
True
1
proof
[(triple1)]
("Bob" "is" "kind" "+")
triple1
Fiona is blue.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "blue" "+")
triple3
Bob is young.
True
2
proof
[(((triple1) -> rule7))]
("Bob" "is" "young" "+")
((triple1) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not young.
False
2
inv-proof
[(((triple1) -> rule7))]
("Bob" "is" "young" "-")
((triple1) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is green.
True
3
proof
[(((((triple1) -> rule7)) -> rule5))]
("Bob" "is" "green" "+")
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is not green.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule5))]
("Bob" "is" "green" "-")
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is not white.
True
4
proof
[(((((((triple1) -> rule7)) -> rule5)) -> rule6))]
("Bob" "is" "white" "-")
((((((triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is not nice.
False
4
inv-proof
[(((((((triple1) -> rule7)) -> rule5)) -> rule4))]
("Bob" "is" "nice" "-")
((((((triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Dave is not young.
Unknown
inv-rconc
[@2: Dave is young.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Dave" "is" "young" "-")
Fiona is young.
Unknown
rconc
[@2: Fiona is young.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Fiona" "is" "young" "+")
Harry is not young.
Unknown
inv-rconc
[@2: Harry is young.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Harry" "is" "young" "-")
Fiona is nice.
Unknown
rconc
[@4: Fiona is nice.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule1 <- rule3 <- FAIL)]]
("Fiona" "is" "nice" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is kind.[(triple1)] Dave is kind.[(triple2)] Fiona is not blue.[(triple3)] Harry is kind.[(triple4)] @1: Bob is young.[(((triple1) -> rule7))] @2: Bob is green.[(((((triple1) -> rule7)) -> rule5))] @3: Bob is nice.[(((((((triple1) -> rule7)) -> rule5)) -> rule4))] Bob is not white.[(((((((triple1) -> rule7)) -> rule5)) -> rule6))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Fiona is not blue.
("Fiona" "is" "blue" "-")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
((((((triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is not white.
("Bob" "is" "white" "-")
((((((triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3