Bob is kind. Bob is red. Dave is quiet. Dave is red. Dave is smart. Fiona is cold. Fiona is rough. If something is smart then it is red. If something is rough then it is young. Young things are red.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
If something is smart then it is red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
If something is rough then it is young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
Young things are red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
Dave is red.
True
1
proof
[(triple4 OR ((triple5) -> rule1))]
("Dave" "is" "red" "+")
triple4
((triple5) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Fiona is not rough.
False
1
inv-proof
[(triple7)]
("Fiona" "is" "rough" "-")
triple7
Fiona is young.
True
2
proof
[(((triple7) -> rule2))]
("Fiona" "is" "young" "+")
((triple7) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is not young.
False
2
inv-proof
[(((triple7) -> rule2))]
("Fiona" "is" "young" "-")
((triple7) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is red.
True
3
proof
[(((((triple7) -> rule2)) -> rule3))]
("Fiona" "is" "red" "+")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is not red.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule3))]
("Fiona" "is" "red" "-")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "young" "-")
Bob is young.
Unknown
rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "young" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Bob is kind.[(triple1)] Bob is red.[(triple2)] Dave is quiet.[(triple3)] Dave is red.[(triple4 OR ((triple5) -> rule1))] Dave is smart.[(triple5)] Fiona is cold.[(triple6)] Fiona is rough.[(triple7)] @1: Fiona is young.[(((triple7) -> rule2))] @2: Fiona is red.[(((((triple7) -> rule2)) -> rule3))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
((triple5) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
Fiona is rough.
("Fiona" "is" "rough" "+")
triple7
Fiona is young.
("Fiona" "is" "young" "+")
((triple7) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2