Bob is rough. Dave is smart. Fiona is round. Gary is white. All rough, kind things are round. All rough things are smart. All red things are rough. All nice things are white. If Bob is smart then Bob is nice. Rough, white things are kind.
Bob is rough.
("Bob" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
All rough, kind things are round.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
All rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
All red things are rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
All nice things are white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If Bob is smart then Bob is nice.
((("Bob" "is" "smart" "+")) -> ("Bob" "is" "nice" "+"))
Rough, white things are kind.
((("something" "is" "rough" "+") ("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
Fiona is round.
True
1
proof
[(triple3)]
("Fiona" "is" "round" "+")
triple3
Fiona is not round.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "round" "-")
triple3
Bob is smart.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not smart.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "smart" "-")
((triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is nice.
True
3
proof
[(((((triple1) -> rule2)) -> rule5))]
("Bob" "is" "nice" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not nice.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule5))]
("Bob" "is" "nice" "-")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
True
4
proof
[(((((((triple1) -> rule2)) -> rule5)) -> rule4))]
("Bob" "is" "white" "+")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is not white.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule5)) -> rule4))]
("Bob" "is" "white" "-")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Dave is not kind.
Unknown
inv-rconc
[@2: Dave is kind.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Dave" "is" "kind" "-")
Fiona is smart.
Unknown
rconc
[@2: Fiona is smart.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Fiona" "is" "smart" "+")
Fiona is not rough.
Unknown
inv-rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is kind.
Unknown
rconc
[@2: Fiona is kind.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Fiona" "is" "kind" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Bob is rough.[(triple1)] Dave is smart.[(triple2)] Fiona is round.[(triple3)] Gary is white.[(triple4)] @1: Bob is smart.[(((triple1) -> rule2))] @2: Bob is nice.[(((((triple1) -> rule2)) -> rule5))] @3: Bob is white.[(((((((triple1) -> rule2)) -> rule5)) -> rule4))] @4: Bob is kind.[(((triple1 ((((((triple1) -> rule2)) -> rule5)) -> rule4)) -> rule6))] @5: Bob is round.[(((triple1 ((triple1 ((((((triple1) -> rule2)) -> rule5)) -> rule4)) -> rule6)) -> rule1))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Fiona is round.
("Fiona" "is" "round" "+")
triple3
Gary is white.
("Gary" "is" "white" "+")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
((triple1 ((((((triple1) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is round.
("Bob" "is" "round" "+")
((triple1 ((triple1 ((((((triple1) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5