Bob is quiet. Dave is kind. Dave is smart. Fiona is young. Gary is blue. Gary is cold. Gary is kind. If Bob is young then Bob is smart. Young, rough people are blue. If someone is quiet and young then they are blue. Young people are cold. All cold people are quiet. If someone is kind and not young then they are quiet. If someone is rough then they are not kind. If Gary is smart and Gary is blue then Gary is not kind. If someone is blue and young then they are rough.
Bob is quiet.
("Bob" "is" "quiet" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
If Bob is young then Bob is smart.
((("Bob" "is" "young" "+")) -> ("Bob" "is" "smart" "+"))
Young, rough people are blue.
((("someone" "is" "young" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
If someone is quiet and young then they are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
Young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
All cold people are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
If someone is kind and not young then they are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "quiet" "+"))
If someone is rough then they are not kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "-"))
If Gary is smart and Gary is blue then Gary is not kind.
((("Gary" "is" "smart" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "kind" "-"))
If someone is blue and young then they are rough.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
Gary is blue.
True
1
proof
[(triple5)]
("Gary" "is" "blue" "+")
triple5
Fiona is not young.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "young" "-")
triple4
Fiona is cold.
True
2
proof
[(((triple4) -> rule4))]
("Fiona" "is" "cold" "+")
((triple4) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is not cold.
False
2
inv-proof
[(((triple4) -> rule4))]
("Fiona" "is" "cold" "-")
((triple4) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is quiet.
True
3
proof
[(((((triple4) -> rule4)) -> rule5))]
("Fiona" "is" "quiet" "+")
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is not quiet.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule5))]
("Fiona" "is" "quiet" "-")
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is blue.
True
5
proof
[(((((((triple4) -> rule4)) -> rule5) triple4) -> rule3))]
("Fiona" "is" "blue" "+")
((((((triple4) -> (rule4 % int3))) -> (rule5 % int2)) triple4) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is not blue.
False
5
inv-proof
[(((((((triple4) -> rule4)) -> rule5) triple4) -> rule3))]
("Fiona" "is" "blue" "-")
((((((triple4) -> (rule4 % int3))) -> (rule5 % int2)) triple4) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is rough.
True
7
proof
[(((((((((triple4) -> rule4)) -> rule5) triple4) -> rule3) triple4) -> rule9))]
("Fiona" "is" "rough" "+")
((((((((triple4) -> (rule4 % int4))) -> (rule5 % int3)) triple4) -> (rule3 % int2)) triple4) -> (rule9 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is not rough.
False
7
inv-proof
[(((((((((triple4) -> rule4)) -> rule5) triple4) -> rule3) triple4) -> rule9))]
("Fiona" "is" "rough" "-")
((((((((triple4) -> (rule4 % int4))) -> (rule5 % int3)) triple4) -> (rule3 % int2)) triple4) -> (rule9 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is not kind.
True
8
proof
[(((((((((((triple4) -> rule4)) -> rule5) triple4) -> rule3) triple4) -> rule9)) -> rule7))]
("Fiona" "is" "kind" "-")
((((((((((triple4) -> (rule4 % int5))) -> (rule5 % int4)) triple4) -> (rule3 % int3)) triple4) -> (rule9 % int2))) -> (rule7 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is cold.
("Fiona" "is" "cold" "+")
int5
Fiona is kind.
False
8
inv-proof
[(((((((((((triple4) -> rule4)) -> rule5) triple4) -> rule3) triple4) -> rule9)) -> rule7))]
("Fiona" "is" "kind" "+")
((((((((((triple4) -> (rule4 % int5))) -> (rule5 % int4)) triple4) -> (rule3 % int3)) triple4) -> (rule9 % int2))) -> (rule7 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is cold.
("Fiona" "is" "cold" "+")
int5
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("Dave" "is" "rough" "-")
Dave is quiet.
Unknown
rconc
[@2: Dave is quiet.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Dave" "is" "quiet" "+")
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "smart" "-")
Bob is blue.
Unknown
rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "blue" "+")
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "cold" "-")
Dave is blue.
Unknown
rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "blue" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Bob is quiet.[(triple1)] Dave is kind.[(triple2)] Dave is smart.[(triple3)] Fiona is young.[(triple4)] Gary is blue.[(triple5)] Gary is cold.[(triple6)] Gary is kind.[(triple7)] @1: Fiona is cold.[(((triple4) -> rule4))] Gary is quiet.[(((triple6) -> rule5))] @2: Fiona is quiet.[(((((triple4) -> rule4)) -> rule5))] @3: Fiona is blue.[(((((((triple4) -> rule4)) -> rule5) triple4) -> rule3))] @4: Fiona is rough.[(((((((((triple4) -> rule4)) -> rule5) triple4) -> rule3) triple4) -> rule9))] @5: Fiona is not kind.[(((((((((((triple4) -> rule4)) -> rule5) triple4) -> rule3) triple4) -> rule9)) -> rule7))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Fiona is young.
("Fiona" "is" "young" "+")
triple4
Gary is blue.
("Gary" "is" "blue" "+")
triple5
Gary is cold.
("Gary" "is" "cold" "+")
triple6
Gary is kind.
("Gary" "is" "kind" "+")
triple7
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple4) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple6) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((((((triple4) -> (rule4 % int3))) -> (rule5 % int2)) triple4) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
((((((((triple4) -> (rule4 % int4))) -> (rule5 % int3)) triple4) -> (rule3 % int2)) triple4) -> (rule9 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is not kind.
("Fiona" "is" "kind" "-")
((((((((((triple4) -> (rule4 % int5))) -> (rule5 % int4)) triple4) -> (rule3 % int3)) triple4) -> (rule9 % int2))) -> (rule7 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is cold.
("Fiona" "is" "cold" "+")
int5