Bob is rough. Dave is red. Fiona is young. Gary is kind. Rough people are young. All round, kind people are rough. If someone is kind then they are round.
Bob is rough.
("Bob" "is" "rough" "+")
Dave is red.
("Dave" "is" "red" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Rough people are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
All round, kind people are rough.
((("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If someone is kind then they are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
Fiona is young.
True
1
proof
[(triple3)]
("Fiona" "is" "young" "+")
triple3
Gary is not kind.
False
1
inv-proof
[(triple4)]
("Gary" "is" "kind" "-")
triple4
Bob is young.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "young" "+")
((triple1) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not young.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "young" "-")
((triple1) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Gary is rough.
True
4
proof
[(((((triple4) -> rule3) triple4) -> rule2))]
("Gary" "is" "rough" "+")
((((triple4) -> (rule3 % int2)) triple4) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is not rough.
False
4
inv-proof
[(((((triple4) -> rule3) triple4) -> rule2))]
("Gary" "is" "rough" "-")
((((triple4) -> (rule3 % int2)) triple4) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is young.
True
5
proof
[(((((((triple4) -> rule3) triple4) -> rule2)) -> rule1))]
("Gary" "is" "young" "+")
((((((triple4) -> (rule3 % int3)) triple4) -> (rule2 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is not young.
False
5
inv-proof
[(((((((triple4) -> rule3) triple4) -> rule2)) -> rule1))]
("Gary" "is" "young" "-")
((((((triple4) -> (rule3 % int3)) triple4) -> (rule2 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is rough.
Unknown
rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "rough" "+")
Dave is not young.
Unknown
inv-rconc
[@2: Dave is young.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Dave" "is" "young" "-")
Fiona is rough.
Unknown
rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "rough" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Bob is rough.[(triple1)] Dave is red.[(triple2)] Fiona is young.[(triple3)] Gary is kind.[(triple4)] @1: Bob is young.[(((triple1) -> rule1))] Gary is round.[(((triple4) -> rule3))] @2: Gary is rough.[(((((triple4) -> rule3) triple4) -> rule2))] @3: Gary is young.[(((((((triple4) -> rule3) triple4) -> rule2)) -> rule1))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Fiona is young.
("Fiona" "is" "young" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple4) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((((triple4) -> (rule3 % int2)) triple4) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((((((triple4) -> (rule3 % int3)) triple4) -> (rule2 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3