Bob is smart. Dave is kind. Fiona is rough. Kind people are rough. If someone is rough then they are red. If someone is smart then they are kind.
Bob is smart.
("Bob" "is" "smart" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Kind people are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If someone is rough then they are red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If someone is smart then they are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
Bob is smart.
True
1
proof
[(triple1)]
("Bob" "is" "smart" "+")
triple1
Bob is not smart.
False
1
inv-proof
[(triple1)]
("Bob" "is" "smart" "-")
triple1
Fiona is red.
True
2
proof
[(((triple3) -> rule2))]
("Fiona" "is" "red" "+")
((triple3) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "kind" "-")
((triple1) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Bob" "is" "rough" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not rough.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Bob" "is" "rough" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is red.
True
4
proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule2))]
("Bob" "is" "red" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is not red.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule2))]
("Bob" "is" "red" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Fiona is not kind.
Unknown
inv-rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is smart.[(triple1)] Dave is kind.[(triple2)] Fiona is rough.[(triple3)] @1: Bob is kind.[(((triple1) -> rule3))] Dave is rough.[(((triple2) -> rule1))] Fiona is red.[(((triple3) -> rule2))] @2: Bob is rough.[(((((triple1) -> rule3)) -> rule1))] Dave is red.[(((((triple2) -> rule1)) -> rule2))] @3: Bob is red.[(((((((triple1) -> rule3)) -> rule1)) -> rule2))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple2) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple3) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3